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

QF_UFBV (Model Validation Track)

Competition results for the QF_UFBV logic in the Model Validation Track.

Page generated on 2023-07-06 16:06:00 +0000

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

Winners

Sequential PerformanceParallel Performance
BitwuzlaBitwuzla

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreTimeout Memout
Bitwuzla 0 411 14080.743 14087.1821 0
Bitwuzla Fixedn 0 411 14200.806 14148.051 0
2022-Bitwuzlan 0 406 4750.445 4701.5464 0
Yices2 0 401 11433.119 11404.25511 0
cvc5 0 388 14939.293 14941.77124 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreTimeout Memout
Bitwuzla 0 41114080.74314087.1821 0
Bitwuzla Fixedn 0 41114200.80614148.051 0
2022-Bitwuzlan 0 4064750.4454701.5464 0
Yices2 0 40111433.11911404.25511 0
cvc5 0 38814939.29314941.77124 0

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