SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

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

UFBVFP (Single Query Track)

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

Page generated on 2023-07-06 16:04:54 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
BitwuzlaBitwuzla Bitwuzla cvc5

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla Fixedn 0 2 222.687 222.71420200 0
Bitwuzla 0 2 223.696 223.85520200 0
cvc5 0 1 0.17 0.1710110 0
2022-z3-4.8.17n 0 1 593.55 593.7810111 0
UltimateEliminator+MathSAT 0 0 0.0 0.000020 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla Fixedn 0 2222.687222.71420200 0
Bitwuzla 0 2223.696223.85520200 0
cvc5 0 10.170.1710110 0
2022-z3-4.8.17n 0 1593.55593.7810111 0
UltimateEliminator+MathSAT 0 00.00.000020 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2022-z3-4.8.17n 0 00.00.0000021 0
cvc5 0 00.00.0000020 0
Bitwuzla 0 00.00.0000020 0
UltimateEliminator+MathSAT 0 00.00.0000020 0
Bitwuzla Fixedn 0 00.00.0000020 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Bitwuzla Fixedn 0 2222.687222.714202000 0
Bitwuzla 0 2223.696223.855202000 0
cvc5 0 10.170.17101100 0
2022-z3-4.8.17n 0 1593.55593.78101101 0
UltimateEliminator+MathSAT 0 00.00.0000200 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 0 10.170.1710110 0
Bitwuzla Fixedn 0 10.6550.65610111 0
Bitwuzla 0 10.6560.65610111 0
2022-z3-4.8.17n 0 00.00.000022 0
UltimateEliminator+MathSAT 0 00.00.000020 0

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