SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

AUFBVDTNIA (Single Query Track)

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

Page generated on 2022-08-10 11:17:44 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5 cvc5 cvc5

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2021-cvc5n 0 3 3599.953 3600.3730353 0
cvc5 0 3 3600.194 3600.3530353 0
z3-4.8.17n 0 2 4858.21 4858.87420264 0
UltimateEliminator+MathSAT 0 0 36.311 27.21400080 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2021-cvc5n 0 33600.2133600.2130353 0
cvc5 0 33600.2843600.2830353 0
z3-4.8.17n 0 24858.674858.70420264 0
UltimateEliminator+MathSAT 0 036.31127.21400080 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2021-cvc5n 0 00.00.0000083 0
cvc5 0 00.00.0000083 0
UltimateEliminator+MathSAT 0 00.00.0000080 0
z3-4.8.17n 0 00.00.0000084 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2021-cvc5n 0 30.170.168303053 0
cvc5 0 30.2150.214303053 0
z3-4.8.17n 0 21200.0751200.071202154 0
UltimateEliminator+MathSAT 0 013.8118.38000350 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2021-cvc5n 0 372.21372.2130353 0
cvc5 0 372.28472.2830353 0
z3-4.8.17n 0 2138.676138.67220265 0
UltimateEliminator+MathSAT 0 036.31127.21400080 0

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