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

mjrty.mlw (file (2.1 kB))

Aggregated proportional method calls:

mjrty.json (Z3 : 13.8 kB, CVC4 : 17.6 kB)

Files:

SMT input file	Callgrind output	Call graph data
Z3 (15.8 kB) CVC4 (15.8 kB)	Z3 (1.5 MB) CVC4 (5.3 MB)	Z3 (27.8 kB) CVC4 (400.4 kB)