SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_NIRA (Single Query Track)

Competition results for the QF_NIRA logic in the Single Query Track.

Results were generated on 2024-07-08

Benchmarks: 2
Time Limit: 1200 seconds
Memory Limit: 20480 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Z3-alphaZ3-alpha-Z3-alphaZ3-alpha

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha015.3790235.4799221011010
cvc50144.03701244.1381791011010
SMTInterpol01837.83575437.2698381011010
Yices200000002020

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha015.3790235.4799221011010
cvc50144.03701244.1381791011010
SMTInterpol01837.83575437.2698381011010
Yices200000002020

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha015.3790235.4799221010100
cvc50144.03701244.1381791010100
SMTInterpol01837.83575437.2698381010100
Yices200000001110

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha015.3790235.4799221010100