SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_FP (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
BitwuzlaBitwuzlaBitwuzla Bitwuzla COLIBRI

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 233 64601.558 64608.458233135983737 0
Bitwuzla 0 233 64757.415 64716.937233135983737 0
2019-Par4n 0 218 73823.401 66246.872218120985252 0
COLIBRI 0 214 68905.01 68911.515214117975656 0
MathSAT5n 0 202 98436.622 98404.631202124786868 0
CVC4 0 202 105364.237 105382.294202119836868 0
z3n 0 164 152777.619 152807.35816410262106104 2

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 233 64606.818 64607.058233135983737 0
Bitwuzla 0 233 64761.195 64715.517233135983737 0
2019-Par4n 0 224 81582.771 64035.242224125994646 0
COLIBRI 0 214 68909.06 68909.645214117975656 0
MathSAT5n 0 202 98448.712 98401.301202124786868 0
CVC4 0 202 105375.917 105379.464202119836868 0
z3n 0 164 152798.749 152802.63816410262106104 2

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 135 13539.167 13539.207135135013537 0
Bitwuzla-fixedn 0 135 13545.55 13546.833135135013537 0
2019-Par4n 0 125 36530.943 24995.623125125014546 0
MathSAT5n 0 124 27252.366 27229.387124124014668 0
CVC4 0 119 36828.685 36830.436119119015168 0
COLIBRI 0 117 29723.275 29723.662117117015356 0
z3n 0 102 63539.433 63542.191021020168104 2

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 99 29451.828 23439.6199909917146 0
Bitwuzla-fixedn 0 98 35461.268 35460.2259809817237 0
Bitwuzla 0 98 35622.029 35576.3119809817237 0
COLIBRI 0 97 23585.785 23585.9849709717356 0
CVC4 0 83 52947.232 52949.0288308318768 0
MathSAT5n 0 78 55596.346 55571.9147807819268 0
z3n 0 62 73659.316 73660.44862062208104 2

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
COLIBRI 0 195 2231.049 2231.535195111847575 0
2019-Par4n 0 186 3051.684 2397.193186102848484 0
Bitwuzla 0 165 3030.418 3017.42216510263105105 0
Bitwuzla-fixedn 0 165 3022.373 3018.5116510263105105 0
CVC4 0 124 4100.027 4100.071247549146146 0
MathSAT5n 0 122 4276.25 4249.6941227745148148 0
z3n 0 60 5490.981 5491.01603921210208 2

n Non-competing.