SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

UFDTLIA (Single Query Track)

Competition results for the UFDTLIA logic in the Single Query Track. Chart

Results were generated on 2026-07-25

Benchmarks: 554
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5cvc5cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5048522657.4022718.714851484690690
cvc5-cvc5-xyz ne0484
(base +0)		20907.1220968.574841483700700
z3-BooledASS ne0447
(base -5)		1667.761722.7944704471070940
SMTInterpol01206522.304769.43121012143303530
cvc5-cvc5-xyz-base n048421617.5221679.144841483700700
z3-BooledASS-base n04522366.912422.4445204521020860
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5048522657.4022718.714851484690690
cvc5-cvc5-xyz ne0484
(base +0)		20907.1220968.574841483700700
z3-BooledASS ne0447
(base -5)		1667.761722.7944704471070940
SMTInterpol01218070.265891.74121012143303530
cvc5-cvc5-xyz-base n048421617.5221679.144841483700700
z3-BooledASS-base n04522366.912422.4445204521020860
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5-cvc5-xyz ne01
(base +0)		596.20596.37110055300
cvc501604.38604.55110055300
SMTInterpol000.000.00000155300
z3-BooledASS ne00
(base +0)		0.000.00000155310
cvc5-cvc5-xyz-base n01611.29611.46110055300
z3-BooledASS-base n000.000.00000155310
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5048422053.0322114.1648404843634360
cvc5-cvc5-xyz ne0483
(base +0)		20310.9120372.2048304833734370
z3-BooledASS ne0447
(base -5)		1667.761722.7944704477334650
SMTInterpol01218070.265891.741210121399343200
cvc5-cvc5-xyz-base n048321006.2321067.6848304833734370
z3-BooledASS-base n04522366.912422.4445204526834570
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
z3-BooledASS ne0440
(base -2)		162.89216.884400440111300
cvc50423480.31532.094230423013100
cvc5-cvc5-xyz ne0423
(base +0)		484.82536.834230423013100
SMTInterpol0106621.20243.281060106044800
z3-BooledASS-base n0442179.35233.404420442111100
cvc5-cvc5-xyz-base n0423483.75535.874230423013100
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver