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

ewd673.mlw (file (511 bytes))

Aggregated proportional method calls:

ewd673.json (Z3 : 14.7 kB, CVC4 : 18.4 kB)

Files:

SMT input file Callgrind output Call graph data
Z3 (6.2 kB)
CVC4 (6.2 kB)
Z3 (1.4 MB)
CVC4 (4.0 MB)
Z3 (95.9 kB)
CVC4 (394.7 kB)