SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2017

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

QF_NRA (Main Track)

Competition results for the QF_NRA division as of Fri Jul 21 10:18:02 GMT

Benchmarks in this division: 11354
Time Limit: 1200s

Winners

Sequential Performance Parallel Performance
Yices2 Yices2

Result table1

Sequential Performance

Solver Error Score Correct Score CPU Time Unsolved
CVC4 0.000 8369.648 299.635 2719
SMTRAT 0.000 9535.994 163.090 2843
Yices2 0.000 10266.475 90.097 1415
veriT+raSAT+Redlog 0.000 9798.022 138.326 2220
z3-4.5.0n 0.000 10208.116 86.746 1603

Parallel Performance

Solver Error Score Correct Score CPU Score WALL Score Unsolved
CVC4 0.000 8369.648 299.778 300.253 2719
SMTRAT 0.000 9535.994 163.093 163.106 2843
Yices2 0.000 10266.475 90.098 90.119 1415
veriT+raSAT+Redlog 0.000 9800.938 153.640 137.550 2217
z3-4.5.0n 0.000 10208.116 86.746 86.800 1603

n. Non-competing.

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