Using a General-Purpose Benchmark Suite for Domain-Specific SMT-solving

Subfolders:

None

Why3ML reference verification file

verifythis_2015_relaxed_prefix.mlw (file (4.1 kB))

Aggregated proportional method calls:

verifythis_2015_relaxed_prefix.json (Z3 : 3.9 kB, CVC4 : 18.7 kB)

Files:

SMT input file	Callgrind output	Call graph data
Z3 (12.4 kB) CVC4 (12.4 kB)	Z3 (1.6 MB) CVC4 (5.2 MB)	Z3 (3.6 kB) CVC4 (449.8 kB)