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_NRA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5cvc5 cvc5 cvc5

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2481 399669.202 361574.005248111641317285222 63
cvc5 0 2424 457936.711 494015.508242411351289342342 0
Yices2 0 2207 706374.673 706393.693220710331174559559 0
z3n 0 2141 711254.639 711998.222214110891052625491 0
SMT-RAT-MCSAT 0 2002 940921.825 940887.41120029881014764728 13
veriT+raSAT+Redlog 0 1772 1213198.016 1213004.7821772816956994994 0
MathSAT5n 0 1587 1449265.144 1449789.7141587465112211791179 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2509422005.372346718.112250911871322257194 63
cvc5 0 2424493909.782493999.278242411351289342342 0
Yices2 0 2207706438.053706374.713220710331174559559 0
z3n 0 2141711686.449711977.232214110891052625491 0
SMT-RAT-MCSAT 0 2002940988.825940862.62120029881014764728 13
veriT+raSAT+Redlog 0 17721213262.8261212982.4621772816956994994 0
MathSAT5n 0 15871449868.0141449737.3641587465112211791179 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2019-Par4n 0 1187210403.901159926.4241187118701121467194 63
cvc5 0 1135231251.989231249.2591135113501641467342 0
z3n 0 1089239100.604239080.551089108902101467491 0
Yices2 0 1033331488.834331477.0181033103302661467559 0
SMT-RAT-MCSAT 0 988372472.063372388.66698898803111467728 13
veriT+raSAT+Redlog 0 816594180.479594005.81981681604831467994 0
MathSAT5n 0 4651016302.7141016229.61465465083414671179 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2019-Par4n 0 132258001.47133191.688132201322171427194 63
cvc5 0 1289109057.793109150.019128901289501427342 0
Yices2 0 1174221349.219221297.6941174011741651427559 0
MathSAT5n 0 1122279965.3279907.75411220112221714271179 0
z3n 0 1052324583.113324893.2841052010522871427491 0
SMT-RAT-MCSAT 0 1014415673.261415630.3511014010143251427728 13
veriT+raSAT+Redlog 0 956465482.346465376.64295609563831427994 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 234617304.63412642.772234611121234420357 63
cvc5 0 219916580.2516556.889219910481151567567 0
Yices2 0 206018191.29618166.57120609821078706706 0
z3n 0 204821152.21721090.4320481050998718709 0
SMT-RAT-MCSAT 0 182325484.50825422.9571823946877943930 13
veriT+raSAT+Redlog 0 171026415.12826370.697171077993110561056 0
MathSAT5n 0 142535121.40935084.2761425407101813411341 0

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