SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

QF_ABVFPLRA (Single Query Track)

Competition results for the QF_ABVFPLRA logic in the Single Query Track.

Page generated on 2021-07-18 17:29:05 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
COLIBRICOLIBRICOLIBRI COLIBRI COLIBRI

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
COLIBRI - fixedn 0 25 33.717 33.8022520500 0
COLIBRI 0 25 34.015 34.0362520500 0
cvc5 0 25 461.359 460.5042520500 0
2020-CVC4n 0 25 1297.533 1296.7692520500 0
MathSAT5n 0 13 1220.011 1220.40413130121 0
2020-MathSAT5n 0 13 1221.498 1221.82313130121 0
Bitwuzla 0 9 2.454 2.657990160 0
2020-COLIBRIn 3 17 2702.078 2702.5351717082 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
COLIBRI - fixedn 0 2533.71733.8022520500 0
COLIBRI 0 2534.01534.0362520500 0
cvc5 0 25461.359460.5042520500 0
2020-CVC4n 0 251297.5331296.7692520500 0
MathSAT5n 0 131220.3411220.34413130121 0
2020-MathSAT5n 0 131221.7981221.80313130121 0
Bitwuzla 0 92.4542.657990160 0
2020-COLIBRIn 3 172702.2082702.4151717082 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
COLIBRI - fixedn 0 2017.94818.01320200050 0
COLIBRI 0 2018.0518.06420200050 0
cvc5 0 20101.231100.28120200050 0
2020-CVC4n 0 20506.701506.8720200050 0
MathSAT5n 0 131220.2061220.20913130751 0
2020-MathSAT5n 0 131221.6531221.65813130751 0
Bitwuzla 0 92.432.5659901150 0
2020-COLIBRIn 3 171489.0221489.10117170352 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
COLIBRI - fixedn 0 515.76915.7895050200 0
COLIBRI 0 515.96415.9725050200 0
cvc5 0 5360.127360.2235050200 0
2020-CVC4n 0 5790.832789.95050200 0
Bitwuzla 0 00.0250.0920005200 0
MathSAT5n 0 00.1350.1360005201 0
2020-MathSAT5n 0 00.1450.1450005201 0
2020-COLIBRIn 0 01213.1861213.3140005202 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
COLIBRI - fixedn 0 2533.71733.8022520500 0
COLIBRI 0 2534.01534.0362520500 0
cvc5 0 22127.363126.4022219333 0
2020-CVC4n 0 21146.393145.382118344 0
MathSAT5n 0 1344.34144.34413130121 0
2020-MathSAT5n 0 1345.79845.80313130121 0
Bitwuzla 0 92.4542.657990160 0
2020-COLIBRIn 3 15159.376159.56715150104 0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.