SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_Strings (Single Query Track)

Competition results for the QF_Strings division in the Single Query Track.

Results were generated on 2024-07-08

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Z3-NoodlerZ3-NoodlerZ3-NoodlerZ3-NoodlerZ3-Noodler

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-Noodler03219529805.06945533033.36176321952136510830460420619
cvc5030457824325.113303827555.7170453045720015104422198421904
Z3-alpha029647448961.923086452019.22236929647189761067130084255849
OSTRICH029331628004.79958336081.8537112939118654107373264432630

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-Noodler03219529805.06945533033.36176321952136510830460420619
cvc5030457824325.113303827555.7170453045720015104422198421904
Z3-alpha029647448961.923086452019.22236929647189761067130084255849
OSTRICH029391730477.350266389509.3319072939118654107373264432630

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-Noodler02136518197.48147720339.69262221365213650253110411587
cvc5020015724379.434646726547.7765032001520015016031104116012
Z3-alpha018976303358.943966305322.75510818976189760264211041232929
OSTRICH018654591073.660837308877.3865081865418654029641104129630

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-Noodler01083011607.58797812693.6691371083001083017621653445
OSTRICH010737139403.68942980631.94539910737010737269216532690
Z3-alpha010671145602.979119146696.467261106710106713352165322220
cvc501044299945.678658101007.94054210442010442564216535582

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-Noodler03210711361.03849614575.65824732107213141079323531700
Z3-alpha02848420390.89549223248.73288628484179971048797407800
cvc502802813125.5674615923.0867012802817921101074462700
OSTRICH027618273676.320469113166.1585642761817144104740504100