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

vacid_0_red_black_trees.mlw (file (9.9 kB))

Aggregated proportional method calls:

vacid_0_red_black_trees.json (Z3 : 3.2 kB, CVC4 : 19.2 kB)

Files:

SMT input file Callgrind output Call graph data
Z3 (10.9 kB)
CVC4 (10.9 kB)
Z3 (1.5 MB)
CVC4 (5.2 MB)
Z3 (44.0 kB)
CVC4 (414.6 kB)
Z3 (7.2 kB)
CVC4 (7.2 kB)
Z3 (1.3 MB)
CVC4 (4.0 MB)
Z3 (82.0 kB)
CVC4 (302.9 kB)
Z3 (8.7 kB)
CVC4 (8.7 kB)
Z3 (1.2 MB)
CVC4 (4.0 MB)
Z3 (79.9 kB)
CVC4 (294.5 kB)
Z3 (5.7 kB)
CVC4 (5.7 kB)
Z3 (1.8 MB)
CVC4 (4.4 MB)
Z3 (86.4 kB)
CVC4 (359.7 kB)
Z3 (13.7 kB)
CVC4 (13.7 kB)
Z3 (1.3 MB)
CVC4 (4.3 MB)
Z3 (87.7 kB)
CVC4 (344.5 kB)
Z3 (5.4 kB)
CVC4 (5.4 kB)
Z3 (1.6 MB)
CVC4 (4.5 MB)
Z3 (111.3 kB)
CVC4 (357.6 kB)
Z3 (6.5 kB)
CVC4 (6.5 kB)
Z3 (1.3 MB)
CVC4 (4.4 MB)
Z3 (83.3 kB)
CVC4 (344.1 kB)
Z3 (6.6 kB)
CVC4 (6.6 kB)
Z3 (1.3 MB)
CVC4 (4.0 MB)
Z3 (80.9 kB)
CVC4 (307.9 kB)
Z3 (9.6 kB)
CVC4 (9.6 kB)
Z3 (1.7 MB)
CVC4 (4.1 MB)
Z3 (17.4 kB)
CVC4 (321.8 kB)
Z3 (16.3 kB)
CVC4 (16.3 kB)
Z3 (1.5 MB)
CVC4 (5.2 MB)
Z3 (41.9 kB)
CVC4 (419.9 kB)
CVC4 (7.7 kB)
Z3 (1.4 MB)
CVC4 (4.5 MB)
Z3 (3.2 kB)
CVC4 (376.1 kB)
Z3 (6.4 kB)
CVC4 (6.4 kB)
Z3 (1.2 MB)
CVC4 (4.0 MB)
Z3 (78.8 kB)
CVC4 (299.2 kB)
Z3 (7.3 kB)
CVC4 (7.3 kB)
Z3 (1.3 MB)
CVC4 (4.0 MB)
Z3 (82.1 kB)
CVC4 (302.9 kB)
Z3 (5.3 kB)
CVC4 (5.3 kB)
Z3 (1.8 MB)
CVC4 (4.5 MB)
Z3 (13.9 kB)
CVC4 (348.2 kB)
Z3 (6.0 kB)
CVC4 (6.0 kB)
Z3 (1.6 MB)
CVC4 (4.5 MB)
Z3 (110.4 kB)
CVC4 (358.4 kB)
Z3 (14.2 kB)
CVC4 (14.2 kB)
Z3 (1.4 MB)
CVC4 (5.0 MB)
Z3 (88.7 kB)
CVC4 (556.5 kB)
Z3 (8.7 kB)
CVC4 (8.7 kB)
Z3 (1.3 MB)
CVC4 (4.1 MB)
Z3 (83.5 kB)
CVC4 (310.8 kB)
Z3 (5.1 kB)
CVC4 (5.1 kB)
Z3 (1.3 MB)
CVC4 (4.1 MB)
Z3 (45.1 kB)
CVC4 (306.0 kB)
Z3 (7.9 kB)
CVC4 (7.9 kB)
Z3 (1.4 MB)
CVC4 (4.5 MB)
Z3 (3.2 kB)
CVC4 (376.1 kB)
Z3 (9.9 kB)
CVC4 (9.9 kB)
Z3 (1.7 MB)
CVC4 (4.1 MB)
Z3 (1.2 kB)
CVC4 (321.4 kB)
Z3 (15.7 kB)
CVC4 (15.7 kB)
Z3 (1.7 MB)
CVC4 (5.1 MB)
Z3 (7.2 kB)
CVC4 (418.0 kB)
Z3 (4.5 kB)
CVC4 (4.5 kB)
Z3 (1.4 MB)
CVC4 (3.8 MB)
Z3 (16.2 kB)
CVC4 (273.2 kB)
Z3 (10.0 kB)
CVC4 (10.0 kB)
Z3 (1.4 MB)
CVC4 (5.1 MB)
Z3 (3.4 kB)
CVC4 (401.8 kB)
Z3 (14.1 kB)
CVC4 (14.1 kB)
Z3 (1.3 MB)
CVC4 (4.3 MB)
Z3 (86.6 kB)
CVC4 (337.6 kB)
Z3 (7.0 kB)
CVC4 (7.0 kB)
Z3 (852.3 kB)
CVC4 (2.9 MB)
Z3 (1.9 kB)
CVC4 (87.3 kB)
Z3 (9.1 kB)
CVC4 (9.1 kB)
Z3 (1.4 MB)
CVC4 (4.7 MB)
Z3 (4.4 kB)
CVC4 (368.5 kB)
Z3 (5.6 kB)
CVC4 (5.6 kB)
Z3 (1.8 MB)
CVC4 (4.5 MB)
Z3 (82.3 kB)
CVC4 (360.2 kB)
Z3 (5.0 kB)
CVC4 (5.0 kB)
Z3 (1.2 MB)
CVC4 (4.1 MB)
Z3 (45.0 kB)
CVC4 (306.6 kB)
Z3 (7.4 kB)
CVC4 (7.4 kB)
Z3 (1.3 MB)
CVC4 (4.0 MB)
Z3 (85.5 kB)
CVC4 (311.2 kB)
Z3 (6.1 kB)
CVC4 (6.1 kB)
Z3 (1.6 MB)
CVC4 (4.5 MB)
Z3 (109.2 kB)
CVC4 (362.4 kB)
Z3 (5.9 kB)
CVC4 (5.9 kB)
Z3 (1.6 MB)
CVC4 (4.5 MB)
Z3 (110.2 kB)
CVC4 (362.4 kB)
Z3 (8.9 kB)
CVC4 (8.9 kB)
Z3 (1.6 MB)
CVC4 (4.7 MB)
Z3 (7.6 kB)
CVC4 (372.2 kB)
Z3 (13.9 kB)
CVC4 (13.9 kB)
Z3 (1.3 MB)
CVC4 (4.3 MB)
Z3 (87.6 kB)
CVC4 (340.5 kB)
Z3 (15.7 kB)
CVC4 (15.7 kB)
Z3 (1.7 MB)
CVC4 (5.1 MB)
Z3 (4.3 kB)
CVC4 (410.1 kB)
Z3 (9.7 kB)
CVC4 (9.7 kB)
Z3 (1.3 MB)
CVC4 (4.1 MB)
Z3 (80.7 kB)
CVC4 (316.5 kB)
Z3 (6.3 kB)
CVC4 (6.3 kB)
Z3 (1.6 MB)
CVC4 (4.5 MB)
Z3 (109.6 kB)
CVC4 (358.4 kB)
Z3 (6.8 kB)
CVC4 (6.8 kB)
Z3 (1.3 MB)
CVC4 (4.4 MB)
Z3 (83.4 kB)
CVC4 (336.4 kB)