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_NRA (Unsat Core Track)

Competition results for the QF_NRA division in the Unsat Core Track.

Page generated on 2019-07-23 17:57:45 +0000

Benchmarks: 243
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel Performance
CVC4-ucCVC4-uc

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreAbstainedTimeout Memout
2018-CVC4 (unsat core)n 0 177859 94980.353 94945.79633 0
CVC4-uc 0 177705 92963.219 92976.35934 0
MathSAT-default 0 174586 113349.612 113361.38641 0
MathSAT-na-ext 0 174518 114119.33 114126.14841 0
Z3n 0 169491 28653.867 28653.9694 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreAbstainedTimeout Memout
2018-CVC4 (unsat core)n 0 17785994990.41394944.32633 0
CVC4-uc 0 17770592972.74992975.19934 0
MathSAT-default 0 174586113355.612113359.49641 0
MathSAT-na-ext 0 174518114124.61114124.26841 0
Z3n 0 16949128654.41728653.7994 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.