SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

QF_UFNRA (Main Track)

Competition results for the QF_UFNRA division as of Fri Jul 13 00:02:11 GMT

Benchmarks in this division : 36
Time limit: 1200s

Winners

Sequential PerformanceParallel Performance
Yices 2.6.0Yices 2.6.0

Result table1

Sequential Performance

Solver Error Score Correctly Solved Score CPU time Score Solved Unsolved
CVC4 0.000 25.863 354.500 23 13
Yices 2.6.0 0.000 32.101 249.123 31 5
veriT+raSAT+Reduce 0.000 15.725 675.749 10 26
z3-4.7.1n 0.000 31.321 9.851 30 6

Parallel Performance

Solver Error Score Correctly Solved Score CPU time Score WALL time Score Solved Unsolved
CVC4 0.00025.863354.500354.5392313
Yices 2.6.0 0.00032.101249.123249.148315
veriT+raSAT+Reduce 0.00015.725675.749675.8501026
z3-4.7.1n 0.00031.3219.8519.852306

n. Non-competing.

1. Scores are computed according to Section 7 of the rules.