SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

QF_Equality+NonLinearArith (Unsat Core Track)

Competition results for the QF_Equality+NonLinearArith division in the Unsat Core Track.

Page generated on 2021-07-18 17:31:25 +0000

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

Logics:

Winners

Sequential PerformanceParallel Performance
cvc5-uccvc5-uc

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreAbstainedTimeout Memout
cvc5-uc 0 80015 1434.877 1435.3030 0
MathSAT5n 0 65084 13764.648 13768.08211 0
z3n 0 27006 1891.262 2413.4352 0
Yices2 0 0 0.65 2.3360 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreAbstainedTimeout Memout
cvc5-uc 0 800151434.8771435.3030 0
MathSAT5n 0 6508413766.06813767.34211 0
z3n 0 270062412.7922413.3352 0
Yices2 0 00.652.3360 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.