SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

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 2020-07-04 11:46:59 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Yices2 Yices2 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 26 4543.262 2873.8072624211 0
Yices2 0 25 10360.485 10361.3472523222 0
Yices2-fixedn 0 25 10528.792 10529.8262523222 0
z3n 0 21 460.452 443.5922119260 0
CVC4 0 12 18502.769 18507.039121021514 0
MathSAT5n 0 8 21742.699 21745.1218621918 0
veriT+raSAT+Redlog 0 1 31193.657 31200.891102626 0
Alt-Ergo 0 0 31200.187 31200.0670002726 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 26 4543.262 2873.8072624211 0
Yices2 0 25 10360.715 10361.3072523222 0
Yices2-fixedn 0 25 10528.992 10529.7962523222 0
z3n 0 21 460.452 443.5922119260 0
CVC4 0 12 18506.259 18506.559121021514 0
MathSAT5n 0 8 21744.389 21744.4018621918 0
veriT+raSAT+Redlog 0 1 31200.007 31200.011102626 0
Alt-Ergo 0 0 31200.187 31200.0670002726 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 24 4543.249 2873.5552424031 0
Yices2 0 23 10359.987 10360.5792323042 0
Yices2-fixedn 0 23 10528.265 10529.0692323042 0
z3n 0 19 460.072 443.2081919080 0
CVC4 0 10 18500.227 18500.527101001714 0
MathSAT5n 0 6 21744.153 21744.1656602118 0
veriT+raSAT+Redlog 0 1 28800.007 28800.011102626 0
Alt-Ergo 0 0 28800.187 28800.0670002726 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
MathSAT5n 0 2 0.236 0.2362022518 0
2019-Par4n 0 2 0.012 0.252202251 0
z3n 0 2 0.38 0.383202250 0
Yices2-fixedn 0 2 0.727 0.727202252 0
Yices2 0 2 0.728 0.728202252 0
CVC4 0 2 6.032 6.0322022514 0
veriT+raSAT+Redlog 0 0 2400.0 2400.00002726 0
Alt-Ergo 0 0 2400.0 2400.00002726 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 19 348.712 271.8921917288 0
z3n 0 17 302.323 285.44817152106 0
Yices2 0 5 549.551 549.5595322222 0
Yices2-fixedn 0 5 549.664 549.6675322222 0
MathSAT5n 0 4 555.855 555.8564222322 0
CVC4 0 3 582.051 582.053122424 0
veriT+raSAT+Redlog 0 1 624.007 624.011102626 0
Alt-Ergo 0 0 624.187 624.0670002726 0

n Non-competing.