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_LinearRealArith (Cloud Track)

Competition results for the QF_LinearRealArith division in the Cloud Track.

Page generated on 2022-08-10 14:49:53 +0000

Benchmarks: 21
Time Limit: 1200 seconds
Memory Limit: N/A GB

Logics: This track is experimental. Solvers are only ranked by performance, but no winner is selected.

Parallel Performance

Solver Error Score Correct ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTS portfolio 3 166814.759165117-20 0
SMTS cube-and-conquer 5 148749.578143119-20 0
SMTS cube-and-conquer (fixed) 6 145681.526142129-20 0
cvc5-cloud 12 423704.17542219-20 0

SAT Performance

Solver Error Score Correct ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTS portfolio 1 51776.0155501150 0
SMTS cube-and-conquer (fixed) 2 22338.1122204150 0
SMTS cube-and-conquer 3 33578.4983303150 0
cvc5-cloud 4 25615.682204150 0

UNSAT Performance

Solver Error Score Correct ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTS portfolio 2 114002.53311011370 0
SMTS cube-and-conquer 2 114139.06911011370 0
SMTS cube-and-conquer (fixed) 4 122862.42512012270 0
cvc5-cloud 8 214488.4952021270 0

24 seconds Performance

Solver Error Score Correct ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTS portfolio 0 7457.81672516-214 0
SMTS cube-and-conquer 0 7482.90571616-214 0
cvc5-cloud 0 1530.56610122-222 0
SMTS cube-and-conquer (fixed) 2 6483.28561517-214 0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.