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

foveoos11_challenge3.mlw (file (1.6 kB))

Aggregated proportional method calls:

foveoos11_challenge3.json (Z3 : 11.0 kB, CVC4 : 17.1 kB)

Files:

SMT input file Callgrind output Call graph data
Z3 (16.6 kB)
CVC4 (16.6 kB)
Z3 (1.6 MB)
CVC4 (5.5 MB)
Z3 (14.5 kB)
CVC4 (595.5 kB)