SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

QF_UFBV (Main Track)

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

Benchmarks in this division : 1224
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 1224.000 17.693 1224 0
CVC4 0.000 1224.000 61.590 1224 0
MathSATn 0.000 1064.211 217.690 1212 12
Yices 2.6.0 0.000 1210.684 121.004 1223 1
z3-4.7.1n 0.000 997.632 262.079 1207 17

Parallel Performance

Solver Error Score Correctly Solved Score CPU time Score WALL time Score Solved Unsolved
Boolector 0.0001224.00017.69317.69512240
CVC4 0.0001224.00061.59061.59312240
MathSATn 0.0001064.211217.691217.706121212
Yices 2.6.0 0.0001210.684121.004121.01212231
z3-4.7.1n 0.000997.632262.080262.105120717

n. Non-competing.

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