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

Subfolders:

None

Why3ML reference verification file

unraveling_a_card_trick.mlw (file (3.5 kB))

Aggregated proportional method calls:

unraveling_a_card_trick.json (Z3 : 16.3 kB, CVC4 : 17.9 kB)

Files:

SMT input file	Callgrind output	Call graph data
Z3 (11.4 kB) CVC4 (11.4 kB)	Z3 (1.5 MB) CVC4 (5.0 MB)	Z3 (35.9 kB) CVC4 (372.3 kB)
Z3 (20.9 kB) CVC4 (20.9 kB)	Z3 (1.6 MB) CVC4 (5.2 MB)	Z3 (44.3 kB) CVC4 (414.2 kB)
Z3 (12.3 kB) CVC4 (12.3 kB)	Z3 (1.5 MB) CVC4 (5.0 MB)	Z3 (27.9 kB) CVC4 (378.6 kB)
Z3 (25.9 kB) CVC4 (25.9 kB)	Z3 (1.5 MB) CVC4 (5.3 MB)	Z3 (51.3 kB) CVC4 (417.1 kB)
Z3 (14.4 kB) CVC4 (14.4 kB)	Z3 (1.3 MB) CVC4 (4.1 MB)	Z3 (83.7 kB) CVC4 (311.7 kB)