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

QF_UFIDL (Unsat Core Track)

Competition results for the QF_UFIDL logic in the Unsat Core Track.

Page generated on 2022-08-10 11:18:51 +0000

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

Winners

Sequential PerformanceParallel Performance
Yices2Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreTimeout Memout
Yices2 0 802882 72820.592 72831.46438 0
MathSATn 0 797716 60435.643 60456.66635 0
2021-MathSAT5n 0 778665 62043.973 62454.55237 0
z3-4.8.17n 0 445009 63224.466 63235.93729 0
smtinterpol 0 185088 112516.056 108352.19384 0
cvc5 0 29766 116283.871 116304.55994 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreTimeout Memout
Yices2 0 80288272825.89272829.86438 0
MathSATn 0 79771660449.06360455.07635 0
2021-MathSAT5n 0 77866562312.44362452.57237 0
z3-4.8.17n 0 44500963229.33663234.76729 0
smtinterpol 0 210908113157.206107652.08782 0
cvc5 0 29766116300.171116300.58994 0

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