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_LIRA (Model Validation Track)

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

Page generated on 2022-08-10 11:19:11 +0000

Benchmarks: 1
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 1 0.11 0.110 0
2020-z3n 0 1 0.353 0.3530 0
z3-4.8.17n 0 1 0.36 0.330 0
MathSATn 0 1 0.471 0.4730 0
cvc5 0 1 4.667 4.6730 0
smtinterpol 0 1 18.191 6.0790 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreTimeout Memout
Yices2 0 10.110.110 0
z3-4.8.17n 0 10.360.330 0
2020-z3n 0 10.3530.3530 0
MathSATn 0 10.4710.4730 0
cvc5 0 14.6674.6730 0
smtinterpol 0 118.1916.0790 0

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