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

bitvector_examples.mlw (file (10.7 kB))

Aggregated proportional method calls:

bitvector_examples.json (Z3 : 10.2 kB, CVC4 : 21.5 kB)

Files:

SMT input file Callgrind output Call graph data
Z3 (13.7 kB)
CVC4 (14.4 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (8.1 kB)
CVC4 (537.6 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.8 MB)
Z3 (34.9 kB)
CVC4 (378.0 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (7.5 kB)
CVC4 (413.9 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (4.8 MB)
Z3 (8.0 kB)
CVC4 (378.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (8.1 kB)
CVC4 (516.4 kB)
Z3 (13.7 kB)
CVC4 (14.4 kB)
Z3 (1.5 MB)
CVC4 (5.2 MB)
Z3 (8.8 kB)
CVC4 (557.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.6 kB)
Z3 (29.0 kB)
CVC4 (29.8 kB)
Z3 (1.5 MB)
CVC4 (5.1 MB)
Z3 (12.8 kB)
CVC4 (536.2 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (518.1 kB)
Z3 (14.0 kB)
CVC4 (14.6 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (34.9 kB)
CVC4 (391.8 kB)
Z3 (13.7 kB)
CVC4 (14.4 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (8.0 kB)
CVC4 (554.5 kB)
Z3 (17.0 kB)
CVC4 (17.7 kB)
Z3 (1.1 MB)
CVC4 (4.4 MB)
Z3 (65.7 kB)
CVC4 (473.5 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (518.1 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.1 MB)
Z3 (35.8 kB)
CVC4 (542.2 kB)
Z3 (17.1 kB)
CVC4 (17.8 kB)
Z3 (1.4 MB)
CVC4 (4.5 MB)
Z3 (65.0 kB)
CVC4 (490.2 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (8.2 kB)
CVC4 (527.7 kB)
Z3 (13.9 kB)
CVC4 (14.6 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.4 kB)
CVC4 (527.1 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (7.7 kB)
CVC4 (516.6 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (518.1 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (517.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (5.1 MB)
Z3 (8.1 kB)
CVC4 (398.4 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (12.8 kB)
CVC4 (517.7 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (34.4 kB)
CVC4 (368.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.4 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (8.5 kB)
CVC4 (516.4 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.2 MB)
Z3 (7.3 kB)
CVC4 (413.9 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (4.7 MB)
Z3 (36.0 kB)
CVC4 (500.9 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (517.9 kB)
Z3 (16.9 kB)
CVC4 (17.6 kB)
Z3 (1.1 MB)
CVC4 (4.6 MB)
Z3 (65.7 kB)
CVC4 (487.1 kB)
Z3 (13.9 kB)
CVC4 (14.6 kB)
Z3 (1.5 MB)
CVC4 (5.2 MB)
Z3 (35.4 kB)
CVC4 (409.8 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.6 kB)
Z3 (14.0 kB)
CVC4 (14.7 kB)
Z3 (1.5 MB)
CVC4 (5.1 MB)
Z3 (35.6 kB)
CVC4 (398.4 kB)
Z3 (15.1 kB)
CVC4 (15.8 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (12.4 kB)
CVC4 (522.9 kB)
Z3 (13.9 kB)
CVC4 (14.6 kB)
Z3 (1.5 MB)
CVC4 (5.2 MB)
Z3 (13.7 kB)
CVC4 (557.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.4 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.2 kB)
CVC4 (517.1 kB)
Z3 (16.8 kB)
CVC4 (17.5 kB)
Z3 (1.4 MB)
CVC4 (4.9 MB)
Z3 (8.1 kB)
CVC4 (536.9 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (34.6 kB)
CVC4 (368.7 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (5.1 MB)
Z3 (8.0 kB)
CVC4 (542.2 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (35.6 kB)
CVC4 (527.7 kB)
Z3 (13.9 kB)
CVC4 (14.6 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (8.0 kB)
CVC4 (538.1 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (35.7 kB)
CVC4 (488.9 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.6 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (5.1 MB)
Z3 (35.6 kB)
CVC4 (542.2 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.4 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (4.9 MB)
Z3 (16.2 kB)
CVC4 (516.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.4 MB)
Z3 (20.9 kB)
CVC4 (467.8 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.5 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (7.8 kB)
CVC4 (412.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (7.2 kB)
CVC4 (368.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (12.8 kB)
CVC4 (518.1 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.1 MB)
Z3 (13.1 kB)
CVC4 (542.2 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (517.7 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (34.4 kB)
CVC4 (368.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (517.7 kB)
Z3 (28.4 kB)
CVC4 (29.3 kB)
Z3 (1.4 MB)
CVC4 (4.8 MB)
Z3 (7.6 kB)
CVC4 (384.3 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (12.3 kB)
CVC4 (368.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (8.2 kB)
CVC4 (411.0 kB)
Z3 (13.9 kB)
CVC4 (14.6 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.6 kB)
CVC4 (537.0 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (8.0 kB)
CVC4 (411.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (8.5 kB)
CVC4 (516.4 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (4.8 MB)
Z3 (7.2 kB)
CVC4 (378.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.7 MB)
Z3 (11.6 kB)
CVC4 (508.4 kB)
Z3 (13.9 kB)
CVC4 (14.6 kB)
Z3 (1.5 MB)
CVC4 (5.2 MB)
Z3 (35.4 kB)
CVC4 (410.6 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.8 MB)
Z3 (7.2 kB)
CVC4 (378.0 kB)
Z3 (17.2 kB)
CVC4 (17.9 kB)
Z3 (1.4 MB)
CVC4 (4.7 MB)
Z3 (7.7 kB)
CVC4 (512.1 kB)
Z3 (13.7 kB)
CVC4 (14.4 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (7.7 kB)
CVC4 (527.1 kB)
Z3 (13.6 kB)
CVC4 (14.3 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (15.8 kB)
CVC4 (410.7 kB)
Z3 (29.2 kB)
CVC4 (30.1 kB)
Z3 (1.5 MB)
CVC4 (5.3 MB)
Z3 (35.9 kB)
CVC4 (569.1 kB)
Z3 (13.7 kB)
CVC4 (14.4 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (8.0 kB)
CVC4 (391.2 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (5.2 MB)
Z3 (15.8 kB)
CVC4 (410.6 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (517.7 kB)
Z3 (13.9 kB)
CVC4 (14.6 kB)
Z3 (1.4 MB)
CVC4 (4.9 MB)
Z3 (13.5 kB)
CVC4 (524.3 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (4.7 MB)
Z3 (36.1 kB)
CVC4 (503.4 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.5 MB)
Z3 (35.2 kB)
CVC4 (487.2 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (34.7 kB)
CVC4 (368.7 kB)
Z3 (13.7 kB)
CVC4 (14.4 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (8.1 kB)
CVC4 (537.0 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (517.7 kB)
Z3 (22.1 kB)
CVC4 (22.8 kB)
Z3 (1.5 MB)
CVC4 (5.4 MB)
Z3 (37.1 kB)
CVC4 (397.7 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (36.0 kB)
CVC4 (518.1 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.5 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (8.5 kB)
CVC4 (516.4 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.4 MB)
CVC4 (4.6 MB)
Z3 (36.2 kB)
CVC4 (494.2 kB)
Z3 (13.8 kB)
CVC4 (14.5 kB)
Z3 (1.5 MB)
CVC4 (5.0 MB)
Z3 (35.9 kB)
CVC4 (516.4 kB)