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

NIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 16 391.879 391.9141612410 0
z3n 0 15 578.667 578.8841512320 0
CVC4 0 12 3069.886 3127.5451211152 0
UltimateEliminator+MathSAT 0 8 84.403 47.82687190 0
Vampire 0 4 15993.967 15701.644041313 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 16 391.879 391.9141612410 0
z3n 0 15 578.667 578.8841512320 0
CVC4 0 12 3127.316 3127.4151211152 0
UltimateEliminator+MathSAT 0 8 84.403 47.82687190 0
Vampire 0 4 15993.967 15701.644041313 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 12 0.673 0.6741212050 0
z3n 0 12 0.74 0.741212050 0
CVC4 0 11 696.05 696.0771111062 0
UltimateEliminator+MathSAT 0 7 57.101 33.617770100 0
Vampire 0 0 14400.0 14400.00001713 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 4 391.206 391.24404130 0
Vampire 0 4 1593.967 1301.644041313 0
z3n 0 3 577.928 578.144303140 0
UltimateEliminator+MathSAT 0 1 27.302 14.209101160 0
CVC4 0 1 2431.266 2431.337101162 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 16 25.433 25.4341612411 0
z3n 0 15 49.324 49.3251512322 0
CVC4 0 10 123.266 123.271109175 0
UltimateEliminator+MathSAT 0 8 84.403 47.82687190 0
Vampire 0 3 338.507 338.5933031414 0

n Non-competing.