SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

AUFNIRA (Single Query Track)

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

Results were generated on 2024-07-08

Benchmarks: 300
Time Limit: 1200 seconds
Memory Limit: 20480 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
cvc50665927.1365245935.2335026626423402320
iProver v3.90419433.8361692445.3885265205224802480
SMTInterpol061237.7603191167.686392606294022421

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50665927.1365245935.2335026626423402320
iProver v3.905237652.458899566.620695205224802480
SMTInterpol061237.7603191167.686392606294022421

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5021080.6741971081.247296220029800
SMTInterpol0000000229800
iProver v3.90000000229820

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50644846.4623284853.98620664064223420
iProver v3.904625704.1186156551.530384604620234200
SMTInterpol061237.7603191167.68639260660234501

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503566.53612970.0519535035026500
iProver v3.9023653.204531191.14653623023027700
SMTInterpol0418.0477738.036069404529100