Using a General-Purpose Benchmark Suite for Domain-Specific SMT-solving

Andrew Healy, Rosemary Monahan, James Power

ACM Symposium on Applied Computing, April 4-8, Pisa, Italy

Subfolders:

None

Why3ML reference verification file

defunctionalization.mlw (file (26.5 kB))

Aggregated proportional method calls:

defunctionalization.json (Z3 : 8.0 kB, CVC4 : 17.4 kB)

Files:

SMT input file Callgrind output Call graph data
Z3 (10.6 kB)
CVC4 (10.6 kB)
Z3 (1.6 MB)
CVC4 (5.1 MB)
Z3 (2.3 kB)
CVC4 (546.9 kB)
Z3 (10.7 kB)
CVC4 (10.7 kB)
Z3 (1.4 MB)
CVC4 (4.8 MB)
Z3 (94.2 kB)
CVC4 (351.1 kB)
Z3 (12.8 kB)
CVC4 (12.8 kB)
Z3 (1.6 MB)
CVC4 (4.1 MB)
Z3 (113.5 kB)
CVC4 (423.9 kB)
Z3 (16.9 kB)
Z3 (1.5 MB)
Z3 (1.5 kB)
Z3 (6.7 kB)
CVC4 (6.7 kB)
Z3 (1.3 MB)
CVC4 (4.9 MB)
Z3 (94.2 kB)
CVC4 (526.5 kB)
Z3 (10.7 kB)
CVC4 (10.7 kB)
Z3 (1.4 MB)
CVC4 (4.9 MB)
Z3 (94.0 kB)
CVC4 (322.8 kB)
Z3 (5.8 kB)
CVC4 (5.8 kB)
Z3 (1.7 MB)
CVC4 (4.8 MB)
Z3 (13.6 kB)
CVC4 (317.2 kB)
Z3 (7.3 kB)
CVC4 (7.3 kB)
Z3 (1.3 MB)
CVC4 (4.3 MB)
Z3 (91.0 kB)
CVC4 (459.3 kB)
Z3 (7.1 kB)
CVC4 (7.1 kB)
Z3 (855.5 kB)
CVC4 (3.0 MB)
Z3 (1.9 kB)
CVC4 (226.9 kB)
Z3 (23.8 kB)
CVC4 (23.8 kB)
Z3 (1.3 MB)
CVC4 (4.4 MB)
Z3 (93.2 kB)
CVC4 (460.4 kB)
Z3 (11.0 kB)
Z3 (1.6 MB)
Z3 (45.9 kB)
Z3 (18.0 kB)
CVC4 (18.0 kB)
Z3 (1.5 MB)
CVC4 (5.1 MB)
Z3 (1.3 kB)
CVC4 (537.5 kB)
Z3 (7.8 kB)
CVC4 (7.8 kB)
Z3 (1.6 MB)
CVC4 (4.8 MB)
Z3 (4.6 kB)
CVC4 (518.3 kB)
Z3 (18.3 kB)
CVC4 (18.3 kB)
Z3 (1.4 MB)
CVC4 (5.1 MB)
Z3 (1.5 kB)
CVC4 (545.1 kB)
Z3 (6.3 kB)
CVC4 (6.3 kB)
Z3 (1.2 MB)
CVC4 (4.0 MB)
Z3 (79.3 kB)
CVC4 (409.3 kB)
Z3 (6.3 kB)
CVC4 (6.3 kB)
Z3 (1.3 MB)
CVC4 (4.6 MB)
Z3 (91.2 kB)
CVC4 (485.1 kB)
Z3 (24.6 kB)
CVC4 (24.6 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (1.2 kB)
CVC4 (503.6 kB)
Z3 (10.3 kB)
CVC4 (10.3 kB)
Z3 (1.3 MB)
CVC4 (4.5 MB)
Z3 (86.9 kB)
CVC4 (487.6 kB)
Z3 (20.6 kB)
CVC4 (20.6 kB)
Z3 (1.7 MB)
CVC4 (4.4 MB)
Z3 (4.3 kB)
CVC4 (458.9 kB)
Z3 (5.8 kB)
CVC4 (5.8 kB)
Z3 (1.7 MB)
CVC4 (4.3 MB)
Z3 (59.0 kB)
CVC4 (335.0 kB)
Z3 (13.8 kB)
CVC4 (13.8 kB)
Z3 (1.3 MB)
CVC4 (4.5 MB)
Z3 (91.4 kB)
CVC4 (486.9 kB)
Z3 (6.9 kB)
CVC4 (6.9 kB)
Z3 (1.4 MB)
CVC4 (4.7 MB)
Z3 (37.1 kB)
CVC4 (488.6 kB)
Z3 (11.7 kB)
Z3 (1.5 MB)
Z3 (10.3 kB)
Z3 (10.0 kB)
CVC4 (10.0 kB)
Z3 (861.3 kB)
CVC4 (3.0 MB)
Z3 (2.7 kB)
CVC4 (231.1 kB)
Z3 (10.0 kB)
CVC4 (10.0 kB)
Z3 (1.3 MB)
CVC4 (4.3 MB)
Z3 (89.8 kB)
CVC4 (451.1 kB)
Z3 (23.1 kB)
CVC4 (23.1 kB)
Z3 (1.7 MB)
CVC4 (4.4 MB)
Z3 (1.3 kB)
CVC4 (459.0 kB)
Z3 (3.0 kB)
CVC4 (3.0 kB)
Z3 (850.3 kB)
CVC4 (2.9 MB)
Z3 (1.6 kB)
CVC4 (127.8 kB)
Z3 (20.8 kB)
CVC4 (20.8 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (100.9 kB)
CVC4 (529.4 kB)
Z3 (11.0 kB)
CVC4 (11.0 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (94.7 kB)
CVC4 (324.0 kB)
Z3 (8.8 kB)
CVC4 (8.8 kB)
Z3 (1.3 MB)
CVC4 (4.1 MB)
Z3 (80.4 kB)
CVC4 (430.5 kB)
Z3 (24.4 kB)
CVC4 (24.4 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (1.2 kB)
CVC4 (527.9 kB)
Z3 (21.3 kB)
CVC4 (21.3 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (3.3 kB)
CVC4 (552.9 kB)
Z3 (6.1 kB)
CVC4 (6.1 kB)
Z3 (1.8 MB)
CVC4 (4.2 MB)
Z3 (13.2 kB)
CVC4 (427.3 kB)
Z3 (3.0 kB)
CVC4 (3.0 kB)
Z3 (1.3 MB)
CVC4 (4.4 MB)
Z3 (11.3 kB)
CVC4 (447.1 kB)
Z3 (14.1 kB)
CVC4 (14.1 kB)
Z3 (1.3 MB)
CVC4 (4.5 MB)
Z3 (56.2 kB)
CVC4 (486.3 kB)
Z3 (24.6 kB)
CVC4 (24.6 kB)
Z3 (1.4 MB)
CVC4 (5.1 MB)
Z3 (3.2 kB)
CVC4 (531.6 kB)
Z3 (6.2 kB)
CVC4 (6.2 kB)
Z3 (856.7 kB)
CVC4 (2.9 MB)
Z3 (1.9 kB)
CVC4 (225.5 kB)
Z3 (24.5 kB)
CVC4 (24.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (1.3 kB)
CVC4 (526.6 kB)
Z3 (20.7 kB)
CVC4 (20.7 kB)
Z3 (869.7 kB)
CVC4 (3.1 MB)
Z3 (3.7 kB)
CVC4 (232.9 kB)
Z3 (6.7 kB)
CVC4 (6.7 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (108.9 kB)
CVC4 (393.5 kB)
Z3 (23.8 kB)
CVC4 (23.8 kB)
Z3 (869.9 kB)
CVC4 (3.1 MB)
Z3 (3.9 kB)
CVC4 (233.3 kB)
Z3 (21.3 kB)
CVC4 (21.3 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (103.2 kB)
CVC4 (538.8 kB)
Z3 (10.8 kB)
CVC4 (10.8 kB)
Z3 (1.4 MB)
CVC4 (4.9 MB)
Z3 (94.1 kB)
CVC4 (320.1 kB)
Z3 (9.9 kB)
CVC4 (9.9 kB)
Z3 (1.7 MB)
CVC4 (4.3 MB)
Z3 (14.9 kB)
CVC4 (470.5 kB)
Z3 (10.0 kB)
CVC4 (10.0 kB)
Z3 (1.3 MB)
CVC4 (4.3 MB)
Z3 (89.8 kB)
CVC4 (451.1 kB)
Z3 (4.0 kB)
CVC4 (4.0 kB)
Z3 (1.4 MB)
CVC4 (4.8 MB)
Z3 (96.5 kB)
CVC4 (505.1 kB)
Z3 (7.8 kB)
CVC4 (7.8 kB)
Z3 (1.6 MB)
CVC4 (4.6 MB)
Z3 (20.7 kB)
CVC4 (487.7 kB)
Z3 (10.5 kB)
CVC4 (10.5 kB)
Z3 (1.5 MB)
CVC4 (4.9 MB)
Z3 (13.8 kB)
CVC4 (528.8 kB)
Z3 (9.7 kB)
CVC4 (9.7 kB)
Z3 (1.7 MB)
CVC4 (4.1 MB)
Z3 (18.0 kB)
CVC4 (425.8 kB)