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

UFIDL (Single Query Track)

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

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

Benchmarks: 20
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-Par4n 0 12 10618.295 10132.642123988 0
z3n 0 11 7791.232 7793.177112995 0
CVC4 0 10 10041.945 10171.0321019108 0
SMTInterpol 0 8 8554.856 8468.986817127 0
SMTInterpol-fixedn 0 8 8559.177 8469.646817127 0
veriT+viten 0 7 12055.816 12057.323707139 1
veriT 0 7 15597.39 15600.8587071312 1
Vampire 0 7 15600.743 15600.7387071313 0
UltimateEliminator+MathSAT 0 0 7250.454 7233.584000206 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 12 10618.295 10132.642123988 0
z3n 0 11 7792.372 7792.837112995 0
CVC4 0 10 10088.555 10170.8021019108 0
SMTInterpol 0 8 8554.856 8468.986817127 0
SMTInterpol-fixedn 0 8 8559.177 8469.646817127 0
veriT+viten 0 7 12056.836 12056.883707139 1
Vampire 0 7 19200.963 15599.2587071313 0
veriT 0 7 15600.31 15600.3087071312 1
UltimateEliminator+MathSAT 0 0 7250.454 7233.584000206 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 3 1018.234 531.949330178 0
z3n 0 2 1200.099 1200.1220185 0
CVC4 0 1 487.112 569.362110198 0
SMTInterpol-fixedn 0 1 1201.48 1200.874110197 0
SMTInterpol 0 1 1201.504 1200.917110197 0
UltimateEliminator+MathSAT 0 0 10.236 6.96000206 0
veriT+viten 0 0 1200.021 1200.024000209 1
veriT 0 0 3600.0 3600.00002012 1
Vampire 0 0 3600.0 3600.00002013 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 9 0.061 0.692909118 0
z3n 0 9 0.828 0.83909115 0
CVC4 0 9 1.443 1.441909118 0
veriT 0 7 2400.31 2400.3087071312 1
veriT+viten 0 7 2400.307 2400.326707139 1
Vampire 0 7 2400.743 2400.7387071313 0
SMTInterpol 0 7 2539.944 2463.015707137 0
SMTInterpol-fixedn 0 7 2544.103 2463.659707137 0
UltimateEliminator+MathSAT 0 0 7211.383 7207.474000206 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 11 216.075 216.828112999 0
z3n 0 11 216.928 216.93112999 0
CVC4 0 9 218.016 218.098909119 0
SMTInterpol 0 8 322.856 236.986817127 0
SMTInterpol-fixedn 0 8 327.177 237.646817127 0
veriT+viten 0 7 264.328 264.3497071310 1
veriT 0 7 312.31 312.3087071312 1
Vampire 0 7 312.743 312.7387071313 0
UltimateEliminator+MathSAT 0 0 194.454 177.584000206 0

n Non-competing.