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

finite_tarski.mlw (file (1.7 kB))

Aggregated proportional method calls:

finite_tarski.json (Z3 : 13.4 kB, CVC4 : 17.4 kB)

Files:

SMT input file	Callgrind output	Call graph data
CVC4 (12.4 kB)	CVC4 (5.2 MB)	CVC4 (549.2 kB)
CVC4 (11.8 kB)	CVC4 (11.0 MB)	CVC4 (212.8 kB)