SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_ABV (Main Track)

Competition results for the QF_ABV division as of Fri Jul 13 00:02:11 GMT

Benchmarks in this division : 15066
Time limit: 1200s

Winners

Sequential PerformanceParallel Performance
BoolectorBoolector

Result table1

Sequential Performance

Solver Error Score Correctly Solved Score CPU time Score Solved Unsolved
Boolector 0.000 14610.671 60.315 15016 50
CVC4 0.000 13024.925 165.756 14925 141
MathSATn 0.000 0.000 131.022 0 15066
Yices 2.6.0 0.000 14446.663 79.138 15012 54
z3-4.7.1n 0.000 13150.377 168.808 14898 168

Parallel Performance

Solver Error Score Correctly Solved Score CPU time Score WALL time Score Solved Unsolved
Boolector 0.00014610.67160.31560.2641501650
CVC4 0.00013024.925165.756175.88314925141
MathSATn 0.0000.000131.022130.965015066
Yices 2.6.0 0.00014446.66379.13879.1431501254
z3-4.7.1n 0.00013150.377168.810168.81714898168

n. Non-competing.

1. Scores are computed according to Section 7 of the rules.