SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_UFNIA (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4Yices2 CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 280 4956.472 4957.3428020179204 0
Yices2-fixedn 0 278 27012.633 27017.858278206722222 0
Yices2 0 278 27050.586 27019.621278206722222 0
2019-CVC4n 0 276 7447.503 7450.44427619977246 0
MathSAT5n 0 267 39792.185 39799.009267187803333 0
z3n 0 259 22582.889 22586.175259182774115 0
Alt-Ergo 0 39 7765.771 7468.795390392616 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 280 4957.312 4957.2528020179204 0
Yices2-fixedn 0 278 27016.013 27016.778278206722222 0
Yices2 0 278 27054.596 27018.621278206722222 0
2019-CVC4n 0 276 7449.963 7450.03427619977246 0
MathSAT5n 0 267 39798.665 39797.739267187803333 0
z3n 0 259 22585.009 22585.575259182774115 0
Alt-Ergo 0 39 7765.771 7468.795390392616 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2-fixedn 0 206 1814.606 1815.05420620609422 0
Yices2 0 206 1853.228 1817.12520620609422 0
CVC4 0 201 2451.707 2451.6632012010994 0
2019-CVC4n 0 199 4899.391 4899.46519919901016 0
MathSAT5n 0 187 24135.714 24134.764187187011333 0
z3n 0 182 14205.962 14206.446182182011815 0
Alt-Ergo 0 0 7748.499 7462.340003006 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
MathSAT5n 0 80 9662.951 9662.9758008022033 0
CVC4 0 79 1209.573 1209.549790792214 0
2019-CVC4n 0 77 2405.366 2405.371770772236 0
z3n 0 77 4547.145 4547.2187707722315 0
Yices2 0 72 19201.367 19201.4967207222822 0
Yices2-fixedn 0 72 19201.407 19201.7237207222822 0
Alt-Ergo 0 39 15.675 5.939390392616 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 279 195.765 195.69727920079217 0
2019-CVC4n 0 275 254.862 254.93527519877259 0
Yices2 0 271 705.052 705.28271199722929 0
Yices2-fixedn 0 271 705.196 705.924271199722929 0
MathSAT5n 0 266 975.488 974.559266187793434 0
z3n 0 252 938.981 939.021252176764830 0
Alt-Ergo 0 39 252.597 196.448390392617 0

n Non-competing.