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

verifythis_fm2012_LRS.mlw (file (15.5 kB))

Aggregated proportional method calls:

verifythis_fm2012_LRS.json (Z3 : 10.8 kB, CVC4 : 19.3 kB)

Files:

SMT input file Callgrind output Call graph data
Z3 (22.0 kB)
CVC4 (22.0 kB)
 Z3 (1.4 MB)
CVC4 (3.1 MB)
 Z3 (7.2 kB)
CVC4 (169.9 kB)
Z3 (22.6 kB)
CVC4 (22.6 kB)
 Z3 (1.5 MB)
CVC4 (5.4 MB)
 Z3 (1.2 kB)
CVC4 (441.5 kB)
Z3 (17.9 kB)
CVC4 (17.9 kB)
 Z3 (1.5 MB)
CVC4 (5.0 MB)
 Z3 (3.1 kB)
CVC4 (419.7 kB)
Z3 (26.7 kB)
CVC4 (26.7 kB)
 Z3 (1.5 MB)
CVC4 (5.5 MB)
 Z3 (4.4 kB)
CVC4 (445.8 kB)
Z3 (17.7 kB)
CVC4 (17.7 kB)
 Z3 (1.4 MB)
CVC4 (5.2 MB)
 Z3 (3.1 kB)
CVC4 (418.4 kB)
Z3 (8.9 kB)
CVC4 (8.9 kB)
 Z3 (864.7 kB)
CVC4 (3.0 MB)
 Z3 (2.6 kB)
CVC4 (90.1 kB)
Z3 (22.4 kB)
CVC4 (22.4 kB)
 Z3 (1.4 MB)
CVC4 (5.1 MB)
 Z3 (7.2 kB)
CVC4 (418.1 kB)
Z3 (15.6 kB)
CVC4 (15.6 kB)
 Z3 (1.5 MB)
CVC4 (5.2 MB)
 Z3 (1.2 kB)
CVC4 (420.8 kB)
Z3 (10.2 kB)
CVC4 (10.2 kB)
 Z3 (1.7 MB)
CVC4 (5.0 MB)
 Z3 (7.4 kB)
CVC4 (413.3 kB)
Z3 (18.3 kB)
CVC4 (18.3 kB)
 Z3 (1.2 MB)
CVC4 (4.7 MB)
 Z3 (80.9 kB)
CVC4 (392.7 kB)
Z3 (9.3 kB)
CVC4 (9.3 kB)
 Z3 (1.6 MB)
CVC4 (5.2 MB)
 Z3 (8.6 kB)
CVC4 (399.0 kB)
Z3 (21.6 kB)
CVC4 (21.6 kB)
 Z3 (1.5 MB)
CVC4 (4.9 MB)
 Z3 (1.5 kB)
CVC4 (413.4 kB)
Z3 (6.2 kB)
CVC4 (6.2 kB)
 Z3 (1.6 MB)
CVC4 (4.7 MB)
 Z3 (14.4 kB)
CVC4 (46.6 kB)
Z3 (21.9 kB)
CVC4 (21.9 kB)
 Z3 (875.7 kB)
CVC4 (3.1 MB)
 Z3 (4.9 kB)
CVC4 (169.5 kB)
Z3 (23.2 kB)
CVC4 (23.2 kB)
 Z3 (1.5 MB)
CVC4 (5.4 MB)
 Z3 (1.2 kB)
CVC4 (432.5 kB)
Z3 (21.0 kB)
CVC4 (21.0 kB)
 Z3 (1.4 MB)
CVC4 (4.0 MB)
 Z3 (6.4 kB)
CVC4 (282.6 kB)
Z3 (24.2 kB)
CVC4 (24.2 kB)
 Z3 (1.5 MB)
CVC4 (5.4 MB)
 Z3 (6.1 kB)
CVC4 (439.6 kB)
Z3 (20.3 kB)
CVC4 (20.3 kB)
 Z3 (1.5 MB)
CVC4 (4.8 MB)
 Z3 (1.2 kB)
CVC4 (393.8 kB)
Z3 (6.7 kB)
CVC4 (6.7 kB)
 Z3 (1.3 MB)
CVC4 (4.9 MB)
 Z3 (84.4 kB)
CVC4 (366.4 kB)