SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_S (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4CVC4 CVC4 CVC4

Note: the division has disagreements

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 922 6697.245 6709.05592244148133 0
Z3str4 0 862 76283.199 76226.7458623834796363 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 922 6697.775 6708.81592244148133 0
Z3str4 0 862 76291.869 76224.5258623834796363 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 441 5488.28 5499.20744144104843 0
Z3str4 0 383 72676.366 72612.351383383054263 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 481 9.495 9.60848104814443 0
Z3str4 0 479 2415.503 2412.174479047944663 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 905 985.719 969.1589054244812020 0
Z3str4 0 858 2022.177 1957.618583794796767 0

n Non-competing.