SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

Participants
Results

FPArith (BVFP, FP, BVFPLRA, FPLRA) - Single Query Track

Competition results for the FPArith (BVFP, FP, BVFPLRA, FPLRA) division in the Single Query Track.

Page generated on 2020-01-29 22:04:58 +0000

Benchmarks: 1422
Time Limit: 2400 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-Z3n 0 994 289976.665 289960.674994194800216148 31
CVC4 0 900 383937.209 384009.537900225675522311 0
z3n 0 806 224884.475 224889.58680624782180163 0
UltimateEliminator+MathSAT 0 179 6600.698 4544.6811793414512431 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Z3n 0 994 289976.665 289960.674994194800216148 31
CVC4 0 900 383937.209 384009.537900225675522311 0
z3n 0 806 224884.475 224889.58680624782180163 0
UltimateEliminator+MathSAT 0 179 6600.698 4544.6811793414512431 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 225 56206.882 56214.60322522501197311 0
2019-Z3n 0 194 23865.882 23869.1319419401016148 31
UltimateEliminator+MathSAT 0 34 1118.363 763.8413434013881 0
z3n 0 24 2180.377 2180.52824240962163 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Z3n 0 800 86936.605 86950.9258000800410148 31
z3n 0 782 91771.227 91751.2487820782204163 0
CVC4 0 675 109319.42 109335.7036750675747311 0
UltimateEliminator+MathSAT 0 145 2923.163 2031.258145014512771 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Z3n 0 843 10008.261 10005.422843164679367305 31
CVC4 0 831 10309.155 10303.754831223608591380 0
z3n 0 699 7794.006 7783.35269921678287272 0
UltimateEliminator+MathSAT 0 179 4859.918 3368.6311793414512431 0

n Non-competing.