SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_UFNRA (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

Benchmarks: 26
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Par4Par4Par4 MathSAT-default Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 25 8616.659 5510.4842523211 0
2018-Yicesn 0 25 15890.008 15891.0412523211 0
Yices 2.6.2 0 24 15942.9 15944.2232422222 0
Z3n 0 20 321.653 321.6872018260 0
CVC4 0 12 34865.887 34871.981121021414 0
MathSAT-default 0 9 40876.429 40879.3039721717 0
MathSAT-na-ext 0 9 41418.613 41421.0369721717 0
veriT+raSAT+Redlog 0 0 62390.64 62401.020002626 0
Alt-Ergo 0 0 62400.0 62400.00002626 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 26 10778.819 5391.9342624200 0
2018-Yicesn 0 25 15890.048 15891.0112523211 0
Yices 2.6.2 0 24 15943.27 15944.1632422222 0
Z3n 0 20 321.653 321.6872018260 0
CVC4 0 12 34870.737 34871.071121021414 0
MathSAT-default 0 9 40878.729 40878.7339721717 0
MathSAT-na-ext 0 9 41420.543 41420.6369721717 0
Alt-Ergo 0 0 62400.0 62400.00002626 0
veriT+raSAT+Redlog 0 0 62400.0 62400.00002626 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 24 10778.806 5391.4452424020 0
2018-Yicesn 0 23 15887.757 15888.7192323031 0
Yices 2.6.2 0 22 15940.743 15941.6362222042 0
Z3n 0 18 321.34 321.3751818080 0
CVC4 0 10 34861.392 34861.726101001614 0
MathSAT-default 0 7 40878.474 40878.4787701917 0
MathSAT-na-ext 0 7 41420.281 41420.3747701917 0
Alt-Ergo 0 0 57600.0 57600.00002626 0
veriT+raSAT+Redlog 0 0 57600.0 57600.00002626 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
MathSAT-default 0 2 0.255 0.2552022417 0
MathSAT-na-ext 0 2 0.261 0.2612022417 0
Z3n 0 2 0.312 0.312202240 0
Par4 0 2 0.012 0.489202240 0
2018-Yicesn 0 2 2.291 2.291202241 0
Yices 2.6.2 0 2 2.527 2.527202242 0
CVC4 0 2 9.345 9.3452022414 0
Alt-Ergo 0 0 4800.0 4800.00002626 0
veriT+raSAT+Redlog 0 0 4800.0 4800.00002626 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 19 264.867 264.8861917273 0
Par4 0 18 397.909 296.6691816288 0
MathSAT-default 0 9 486.729 486.7339721717 0
MathSAT-na-ext 0 5 554.545 554.5535322121 0
2018-Yicesn 0 4 555.062 555.0664222222 0
Yices 2.6.2 0 4 557.89 557.8934222222 0
CVC4 0 2 585.345 585.3452022424 0
Alt-Ergo 0 0 624.0 624.00002626 0
veriT+raSAT+Redlog 0 0 624.0 624.00002626 0

n Non-competing.