SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

UFBV (Single Query Track)

Competition results for the UFBV division in the Single Query Track.

Page generated on 2020-07-04 11:46:59 +0000

Benchmarks: 72
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4 CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2018-Z3n 0 50 26465.515 26470.1835018322222 0
2019-Par4n 0 50 26527.12 26468.8875018322222 0
z3n 0 49 27629.809 27634.2554918312323 0
CVC4 0 27 36606.133 37946.924270274526 0
UltimateEliminator+MathSAT 0 6 5022.737 4853.305606663 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 5026527.1226468.8875018322222 0
2018-Z3n 0 5026469.42526469.4435018322222 0
z3n 0 4927632.83927632.8454918312323 0
CVC4 0 2737777.53437945.354270274526 0
UltimateEliminator+MathSAT 0 65022.7374853.305606663 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 182.1632.164181805423 0
2019-Par4n 0 181.3522.844181805422 0
2018-Z3n 0 183.0063.007181805422 0
UltimateEliminator+MathSAT 0 0890.169828.629000723 0
CVC4 0 010802.00710802.0070007226 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 321325.7671266.043320324022 0
2018-Z3n 0 321266.4181266.436320324022 0
z3n 0 312430.6762430.681310314123 0
CVC4 0 275947.7315968.374270274526 0
UltimateEliminator+MathSAT 0 6122.01682.416606663 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
z3n 0 49584.839584.8454918312323 0
2019-Par4n 0 49614.22588.3384918312323 0
2018-Z3n 0 49588.933588.9374918312323 0
CVC4 0 151251.7471251.761150155747 0
UltimateEliminator+MathSAT 0 6451.845346.457606667 0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.