SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

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 UNSATUnsolvedAbstainedTimeout 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 ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 2610778.8195391.9342624200 0
2018-Yicesn 0 2515890.04815891.0112523211 0
Yices 2.6.2 0 2415943.2715944.1632422222 0
Z3n 0 20321.653321.6872018260 0
CVC4 0 1234870.73734871.071121021414 0
MathSAT-default 0 940878.72940878.7339721717 0
MathSAT-na-ext 0 941420.54341420.6369721717 0
Alt-Ergo 0 062400.062400.00002626 0
veriT+raSAT+Redlog 0 062400.062400.00002626 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2410778.8065391.4452424020 0
2018-Yicesn 0 2315887.75715888.7192323031 0
Yices 2.6.2 0 2215940.74315941.6362222042 0
Z3n 0 18321.34321.3751818080 0
CVC4 0 1034861.39234861.726101001614 0
MathSAT-default 0 740878.47440878.4787701917 0
MathSAT-na-ext 0 741420.28141420.3747701917 0
Alt-Ergo 0 057600.057600.00002626 0
veriT+raSAT+Redlog 0 057600.057600.00002626 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
MathSAT-default 0 20.2550.2552022417 0
MathSAT-na-ext 0 20.2610.2612022417 0
Z3n 0 20.3120.312202240 0
Par4 0 20.0120.489202240 0
2018-Yicesn 0 22.2912.291202241 0
Yices 2.6.2 0 22.5272.527202242 0
CVC4 0 29.3459.3452022414 0
Alt-Ergo 0 04800.04800.00002626 0
veriT+raSAT+Redlog 0 04800.04800.00002626 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Z3n 0 19264.867264.8861917273 0
Par4 0 18397.909296.6691816288 0
MathSAT-default 0 9486.729486.7339721717 0
MathSAT-na-ext 0 5554.545554.5535322121 0
2018-Yicesn 0 4555.062555.0664222222 0
Yices 2.6.2 0 4557.89557.8934222222 0
CVC4 0 2585.345585.3452022424 0
Alt-Ergo 0 0624.0624.00002626 0
veriT+raSAT+Redlog 0 0624.0624.00002626 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.