SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

QF_ABV (Single Query Track)

Competition results for the QF_ABV logic in the Single Query Track.

Page generated on 2021-07-18 17:29:05 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
BitwuzlaBitwuzlaBitwuzla Bitwuzla Bitwuzla

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 2860 37018.143 36994.648286019229382020 0
2020-Bitwuzlan 0 2859 37954.817 37938.833285919229372121 0
2020-Yices2-fixedn 0 2850 59372.453 59339.177285019179333030 0
2020-Yices2n 0 2849 59218.531 59232.236284919179323131 0
Yices2 0 2847 59801.917 59796.85284719179303333 0
MathSAT5n 0 2807 111382.887 111464.888280718929157372 1
z3n 0 2782 139407.319 139458.006278218779059898 0
cvc5 0 2764 136635.116 159245.24527641863901116116 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 286037020.35336994.088286019229382020 0
2020-Bitwuzlan 0 285937956.50737937.733285919229372121 0
2020-Yices2-fixedn 0 285059376.64359337.527285019179333030 0
2020-Yices2n 0 284959223.42159230.936284919179323131 0
Yices2 0 284759805.01759795.54284719179303333 0
MathSAT5n 0 2807111477.387111461.528280718929157372 1
z3n 0 2782139476.939139453.456278218779059898 0
cvc5 0 2764159125.882159239.87527641863901116116 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Bitwuzla 0 19226200.1366168.776192219220195720 0
2020-Bitwuzlan 0 19227134.5267115.1192219220195721 0
2020-Yices2n 0 191716154.89716156.039191719170695731 0
2020-Yices2-fixedn 0 191716152.48316159.026191719170695730 0
Yices2 0 191716278.28416289.491191719170695733 0
MathSAT5n 0 189249670.03249672.6351892189203195772 1
z3n 0 187764332.46664306.6661877187704695798 0
cvc5 0 186380659.2280780.87718631863060957116 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Bitwuzla 0 93830820.21730825.312938093819192320 0
2020-Bitwuzlan 0 93730821.98130822.632937093720192321 0
2020-Yices2-fixedn 0 93343224.1643178.501933093324192330 0
2020-Yices2n 0 93243068.52343074.896932093225192331 0
Yices2 0 93043526.73443506.049930093027192333 0
MathSAT5n 0 91561807.35561788.894915091542192372 1
z3n 0 90575144.47375146.789905090552192398 0
cvc5 0 90178466.66278458.9989010901561923116 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 27973377.3043348.502279718869118383 0
2020-Bitwuzlan 0 27903409.3033412.263279018809109090 0
2020-Yices2-fixedn 0 27673894.8243903.50827671881886113113 0
2020-Yices2n 0 27673901.5123904.79327671881886113113 0
Yices2 0 27673905.6863920.28727671881886113113 0
MathSAT5n 0 27076406.8346386.01527071836871173172 1
z3n 0 27055715.6415688.3827051838867175175 0
cvc5 0 26829014.2628930.82526821818864198198 0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.