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_LinearIntArith (Parallel Track)

Competition results for the QF_LinearIntArith division in the Parallel Track.

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

Benchmarks: 84
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 cube-and-conquer (fixed) 55 1684273.4851615173-50 0
SMTS cube-and-conquer 56 1686714.7641616073-50 0
SMTS portfolio 56 1587736.5171515074-50 0

SAT Performance

Solver Error Score Correct ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTS cube-and-conquer (fixed) 26 1534713.5441515030390 0
SMTS cube-and-conquer 29 1636152.9511616029390 0
SMTS portfolio 29 1537171.5921515030390 0

UNSAT Performance

Solver Error Score Correct ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTS cube-and-conquer 27 030161.81300027570 0
SMTS portfolio 27 030164.92500027570 0
SMTS cube-and-conquer (fixed) 29 129159.94110126570 0

24 seconds Performance

Solver Error Score Correct ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTS portfolio 0 111990.7881111078-578 0
SMTS cube-and-conquer 0 82020.33888081-581 0
SMTS cube-and-conquer (fixed) 0 72025.1377082-582 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.