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_AUFBV (Main Track)

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

Benchmarks in this division : 31
Time limit: 1200s

Winners

Sequential PerformanceParallel Performance
CVC4CVC4

Result table1

Sequential Performance

Solver Error Score Correctly Solved Score CPU time Score Solved Unsolved
Boolector 0.000 31.000 0.700 31 0
CVC4 0.000 31.000 0.311 31 0
MathSATn 0.000 0.000 0.081 0 31
Yices 2.6.0 0.000 31.000 0.391 31 0
z3-4.7.1n 0.000 31.000 0.761 31 0

Parallel Performance

Solver Error Score Correctly Solved Score CPU time Score WALL time Score Solved Unsolved
Boolector 0.00031.0000.7000.701310
CVC4 0.00031.0000.3110.311310
MathSATn 0.0000.0000.0810.080031
Yices 2.6.0 0.00031.0000.3910.391310
z3-4.7.1n 0.00031.0000.7610.626310

n. Non-competing.

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