SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_BVFP (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

Benchmarks: 516
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Par4Par4Par4 Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 516 5822.449 2086.41351622828800 0
2018-CVC4n 0 515 5865.972 5860.39251522828711 0
CVC4 0 515 6604.469 6597.53151522828711 0
Z3n 0 511 28689.085 28669.59151122828355 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 516 5822.449 2086.41351622828800 0
2018-CVC4n 0 515 5865.972 5860.39251522828711 0
CVC4 0 515 6604.599 6597.49151522828711 0
Z3n 0 511 28690.455 28669.36151122828355 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 228 1144.94 450.64822822802880 0
2018-CVC4n 0 228 607.298 606.48122822802881 0
CVC4 0 228 1517.928 1512.14422822802881 0
Z3n 0 228 2292.159 2287.85422822802885 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 288 4677.509 1635.76428802882280 0
CVC4 0 287 5086.671 5085.34828702872291 0
2018-CVC4n 0 287 5258.674 5253.91128702872291 0
Z3n 0 283 26398.296 26381.50728302832335 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 500 1739.911 979.5545002252751616 0
CVC4 0 498 1619.341 1611.9114982242741818 0
2018-CVC4n 0 498 1703.087 1697.3074982252731818 0
Z3n 0 421 3007.762 2984.1034212112109595 0

n Non-competing.