SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

ABVFP (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 15 13645.288 13647.657151321511 0
2018-CVC4n 0 15 13710.212 13712.736151321510 0
UltimateEliminator+MathSAT 0 10 101.942 71.84310100200 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 15 13647.258 13647.247151321511 0
2018-CVC4n 0 15 13712.072 13712.266151321510 0
UltimateEliminator+MathSAT 0 10 101.942 71.84310100200 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 13 3.246 3.242131301711 0
2018-CVC4n 0 13 3.626 3.623131301710 0
UltimateEliminator+MathSAT 0 10 46.535 32.60810100200 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 2 0.144 0.1442022810 0
CVC4 0 2 0.276 0.2752022811 0
UltimateEliminator+MathSAT 0 0 6.538 4.597000300 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 15 291.992 291.987151321512 0
2018-CVC4n 0 15 311.042 311.045151321512 0
UltimateEliminator+MathSAT 0 10 101.942 71.84310100200 0

n Non-competing.