SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

QF_NRA (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5Z3++ cvc5 cvc5

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3++-fixedn 0 2641 379531.82 379433.129264113401301267265 0
2019-Par4n 0 2629 394912.029 356695.171262912921337279221 58
cvc5 0 2545 525901.735 526314.738254512441301363363 0
NRA-LS 0 2488 550489.833 551413.5652488119812904205 0
Yices2 0 2341 702255.323 702324.97234111501191567567 0
z3-4.8.17n 0 2275 666874.65 666955.286227512291046633499 0
SMT-RAT-MCSAT 22.06 0 2189 895361.649 895423.466218911231066719674 21
veriT+raSAT+Redlog 0 1879 1206512.928 1206107.22118799059741029989 0
MathSATn 0 1544 1671561.013 1671677.8351544417112713641364 0
Z3++ 6 2634 379866.348 379759.488263413331301274264 1

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2650412116.989346590.821265013101340258200 58
Z3++-fixedn 0 2641379553.38379423.299264113401301267265 0
cvc5 0 2545526363.395526298.488254512441301363363 0
NRA-LS 0 2488550607.043551413.4052488119812904205 0
Yices2 0 2341702330.553702302.83234111501191567567 0
z3-4.8.17n 0 2275666962.06666934.046227512291046633499 0
SMT-RAT-MCSAT 22.06 0 2189895429.739895399.226218911231066719674 21
veriT+raSAT+Redlog 0 18791206582.3281206082.81118799059741029989 0
MathSATn 0 15441671701.0331671625.8551544417112713641364 0
Z3++ 6 2634379887.798379749.928263413331301274264 1

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Z3++-fixedn 0 1340138024.587137945.426134013400901478265 0
Z3++ 0 1333139336.035139236.716133313330971478264 1
2019-Par4n 0 1310213683.539169246.7671310131001201478200 58
cvc5 0 1244270666.703270732.5251244124401861478363 0
z3-4.8.17n 0 1229212691.942212695.0261229122902011478499 0
NRA-LS 0 1198306992.76307433.82311981198023214785 0
Yices2 0 1150343815.982343799.5171150115002801478567 0
SMT-RAT-MCSAT 22.06 0 1123372615.186372598.7151123112303071478674 21
veriT+raSAT+Redlog 0 905598863.169598592.93590590505251478989 0
MathSATn 0 4171228570.0741228571.6374174170101314781364 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2019-Par4n 0 134066433.4545344.054134001340281540200 58
Z3++-fixedn 0 1301109996.301109945.301130101301671540265 0
cvc5 0 1301123696.692123565.963130101301671540363 0
NRA-LS 0 1290114879.042114971.7121290012907815405 0
Yices2 0 1191226514.571226503.3131191011911771540567 0
MathSATn 0 1127311130.959311054.21911270112724115401364 0
SMT-RAT-MCSAT 22.06 0 1066393704.309393689.7911066010663021540674 21
z3-4.8.17n 0 1046329665.195329633.3891046010463221540499 0
veriT+raSAT+Redlog 0 974475719.159475489.87697409743941540989 0
Z3++ 6 1301108760.907108722.226130101301671540264 1

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 248316782.93312793.51248312281255425367 58
cvc5 0 227118421.74918364.297227111251146637637 0
Z3++-fixedn 0 227017686.37217632.441227011741096638638 0
NRA-LS 0 225819069.89118991.231225810841174650650 0
Yices2 0 223917320.31217289.707223911171122669669 0
z3-4.8.17n 0 221519732.44119693.745221512001015693693 0
SMT-RAT-MCSAT 22.06 0 199124874.12724834.23219911065926917896 21
veriT+raSAT+Redlog 0 179926907.43626854.311179985994011091069 0
MathSATn 0 138839519.32139474.8761388365102315201520 0
Z3++ 6 226617647.39317613.101226611681098642635 1

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