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

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

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

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

Logics:

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 UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 2481 399669.202 361574.0052481116413172850222 63
cvc5 0 2424 457936.711 494015.5082424113512893420342 0
Yices2 0 2207 706374.673 706393.6932207103311745590559 0
z3n 0 2141 711254.639 711998.2222141108910526250491 0
SMT-RAT-MCSAT 0 2002 940921.825 940887.411200298810147640728 13
veriT+raSAT+Redlog 0 1772 1213198.016 1213004.78217728169569940994 0
MathSAT5n 0 1587 1449265.144 1449789.71415874651122117901179 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 2509422005.372346718.1122509118713222570194 63
cvc5 0 2424493909.782493999.2782424113512893420342 0
Yices2 0 2207706438.053706374.7132207103311745590559 0
z3n 0 2141711686.449711977.2322141108910526250491 0
SMT-RAT-MCSAT 0 2002940988.825940862.621200298810147640728 13
veriT+raSAT+Redlog 0 17721213262.8261212982.46217728169569940994 0
MathSAT5n 0 15871449868.0141449737.36415874651122117901179 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout 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 UNSATUnsolvedAbstainedTimeout 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 UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 234617304.63412642.7722346111212344200357 63
cvc5 0 219916580.2516556.8892199104811515670567 0
Yices2 0 206018191.29618166.571206098210787060706 0
z3n 0 204821152.21721090.43204810509987180709 0
SMT-RAT-MCSAT 0 182325484.50825422.95718239468779430930 13
veriT+raSAT+Redlog 0 171026415.12826370.6971710779931105601056 0
MathSAT5n 0 142535121.40935084.27614254071018134101341 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.