SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

Equality+MachineArith (Single Query Track)

Competition results for the Equality+MachineArith division in the Single Query Track.

Page generated on 2022-08-10 11:17:44 +0000

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5cvc5 cvc5 cvc5

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
z3-4.8.17n 0 1460 2647289.743 2655840.30914603361124235202128 12
cvc5 0 1385 2728354.012 2805353.60413853331052242702148 0
2021-cvc5n 0 994 957278.171 1804299.248994249745159712211378 0
Bitwuzla 0 424 670917.812 671049.654424214038132575539 0
UltimateEliminator+MathSAT 0 34 1057160.991 1047799.54334201437780840 5

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
z3-4.8.17n 0 14602655764.5932655748.33914603361124235202128 12
cvc5 0 13852795672.0782805243.11413853331052242702148 0
2021-cvc5n 0 9941798694.0831804225.128994249745159712211378 0
Bitwuzla 0 424671018.952671026.074424214038132575539 0
UltimateEliminator+MathSAT 0 341057163.2111047799.43334201437780840 5

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
z3-4.8.17n 0 336222004.033221984.356336336019032862128 12
cvc5 0 333197600.975201658.285333333019332862148 0
2021-cvc5n 0 249280957.502283684.696249249027732861378 0
Bitwuzla 0 21113034.207113035.605212102313560539 0
UltimateEliminator+MathSAT 0 2087625.15686061.619202005063286840 5

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
z3-4.8.17n 0 11241197772.5591197678.154112401124103316552128 12
cvc5 0 10521354750.3931358800.527105201052110516552148 0
2021-cvc5n 0 745271140.153272994.576745074521528521378 0
Bitwuzla 0 40369584.29169589.0674030403723337539 0
UltimateEliminator+MathSAT 0 14371820.731367233.1551401421431655840 5

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
z3-4.8.17n 0 128461644.46961548.8031284303981252802436 12
cvc5 0 99868259.57868241.74899888910281402770 0
2021-cvc5n 0 74345061.01345033.79274388655184812211822 0
Bitwuzla 0 31216573.36916576.101312192939252575651 0
UltimateEliminator+MathSAT 0 2937924.50932339.98629181137830977 5

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.