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

QF_ABVFPLRA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5COLIBRI cvc5 COLIBRI

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 0 25 401.889 401.9532520500 0
2021-cvc5n 0 25 411.635 411.6792520500 0
COLIBRI 0 24 1246.214 1238.2892420411 0
z3-4.8.17n 0 19 12329.332 12331.4881915466 0
MathSATn 0 14 1214.596 1214.98814140110 0
Bitwuzla 0 9 2.31 2.441990160 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 0 25401.889401.9532520500 0
2021-cvc5n 0 25411.635411.6792520500 0
COLIBRI 0 241246.2141238.2892420411 0
z3-4.8.17n 0 1912330.34212331.1981915466 0
MathSATn 0 141214.5961214.98814140110 0
Bitwuzla 0 92.312.441990160 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
COLIBRI 0 2030.85822.93220200051 0
cvc5 0 20130.867130.89820200050 0
2021-cvc5n 0 20157.807157.82320200050 0
z3-4.8.17n 0 1510300.11110300.97715150556 0
MathSATn 0 141213.1491213.53614140650 0
Bitwuzla 0 92.2872.3849901150 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2021-cvc5n 0 5253.828253.8565050200 0
cvc5 0 5271.022271.0565050200 0
COLIBRI 0 41215.3561215.3564041201 0
z3-4.8.17n 0 42030.2312030.2214041206 0
Bitwuzla 0 00.0230.0570005200 0
MathSATn 0 01.4471.4520005200 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
COLIBRI 0 2470.21462.2892420411 0
2021-cvc5n 0 21137.812137.8172118344 0
cvc5 0 21139.932139.9422118344 0
MathSATn 0 1348.08648.09813130121 0
Bitwuzla 0 92.312.441990160 0
z3-4.8.17n 0 9470.135470.1349811616 0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.