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_AUFNIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-MathSAT-defaultn 0 9 3.653 3.65392700 0
MathSAT5n 0 9 3.845 3.84592700 0
z3n 0 9 22.376 22.37892700 0
CVC4 0 9 23.656 23.66392700 0
Alt-Ergo 0 7 3371.743 862.29470720 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-MathSAT-defaultn 0 9 3.653 3.65392700 0
MathSAT5n 0 9 3.845 3.84592700 0
z3n 0 9 22.376 22.37892700 0
CVC4 0 9 23.656 23.66392700 0
Alt-Ergo 0 7 3371.743 862.29470720 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-MathSAT-defaultn 0 2 0.54 0.5422070 0
MathSAT5n 0 2 0.56 0.5622070 0
CVC4 0 2 3.343 3.34222070 0
z3n 0 2 21.391 21.39322070 0
Alt-Ergo 0 0 282.303 83.60200090 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 7 0.985 0.98570720 0
2019-MathSAT-defaultn 0 7 3.113 3.11370720 0
MathSAT5n 0 7 3.285 3.28570720 0
CVC4 0 7 20.314 20.3270720 0
Alt-Ergo 0 7 3089.44 778.69170720 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-MathSAT-defaultn 0 9 3.653 3.65392700 0
MathSAT5n 0 9 3.845 3.84592700 0
z3n 0 9 22.376 22.37892700 0
CVC4 0 9 23.656 23.66392700 0
Alt-Ergo 0 1 237.92 203.63310188 0

n Non-competing.