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

gcd_bezout.mlw (file (969 bytes))

Aggregated proportional method calls:

gcd_bezout.json (Z3 : 5.4 kB, CVC4 : 21.2 kB)

Files:

SMT input file Callgrind output Call graph data
Z3 (11.2 kB)
CVC4 (11.8 kB)
 Z3 (1.5 MB)
CVC4 (5.1 MB)
 Z3 (1.5 kB)
CVC4 (421.2 kB)