QF_Equality+LinearArith (Unsat Core Track)

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

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

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

Logics:

• QF_ALIA : 30 benchmarks
• QF_AUFLIA : 300 benchmarks
• QF_UFDTLIRA : 17 benchmarks
• QF_UFIDL : 113 benchmarks
• QF_UFLIA : 16 benchmarks
• QF_UFLRA : 101 benchmarks

Winners

Sequential Performance	Parallel Performance
Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
MathSAT5n	0	858722	59814.437	59839.68		32	0
2020-Yices2-fixedn	0	814234	74035.403	74048.059		42	0
Yices2	0	814234	75150.362	75162.454		42	0
2020-z3n	0	456356	85540.187	85554.321		59	0
SMTInterpol	0	371701	102530.616	98995.331		70	0
SMTInterpol-remus	0	365439	160585.778	153953.047		88	0
z3n	0	333851	102081.846	102098.419		66	0
2020-CVC4-ucn	0	204838	102555.808	102570.241		69	0
cvc5-uc	0	45192	120273.425	120291.003		95	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
MathSAT5n	0	858722	59827.477	59838.43		32	0
2020-Yices2-fixedn	0	814234	74040.103	74046.449		42	0
Yices2	0	814234	75155.612	75161.044		42	0
2020-z3n	0	456356	85549.217	85551.951		59	0
SMTInterpol-remus	0	396803	161131.678	152651.437		69	0
SMTInterpol	0	382053	102583.866	98907.361		69	0
z3n	0	333851	102089.356	102095.459		66	0
2020-CVC4-ucn	0	204838	102566.948	102567.471		69	0
cvc5-uc	0	45192	120287.925	120286.673		95	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.