| Home | • | Rules | • | Benchmarks | • | Tools | • | Specs | • | Participants | • | Results | • | SMT-LIB | • | Previous |
|---|
Competition results as of Fri Jul 13 00:02:11 GMT
| Logic | Solvers | Benchmarks | # pairs Complete | % Complete | Order (sequential performance) |
| Order (parallel performance) | |||||
| ABVFP | 1 | 1 | 1 | 100 | CVC4 |
| CVC4 | |||||
| ALIA | 5 | 42 | 210 | 100 | z3-4.7.1n; CVC4; Alt-Ergo; veriT; Vampire 4.3 |
| z3-4.7.1n; CVC4; Alt-Ergo; Vampire 4.3; veriT | |||||
| AUFBVDTLIA | 1 | 1709 | 1709 | 100 | CVC4 |
| CVC4 | |||||
| AUFDTLIA | 2 | 728 | 1456 | 100 | CVC4; Vampire 4.3 |
| CVC4; Vampire 4.3 | |||||
| AUFLIA | 5 | 4 | 20 | 100 | CVC4; veriT; z3-4.7.1n; Alt-Ergo; Vampire 4.3 |
| CVC4; veriT; z3-4.7.1n; Alt-Ergo; Vampire 4.3 | |||||
| AUFLIRA | 5 | 20011 | 100055 | 100 | z3-4.7.1n; CVC4; Alt-Ergo; Vampire 4.3; veriT |
| z3-4.7.1n; CVC4; Vampire 4.3; Alt-Ergo; veriT | |||||
| AUFNIRA | 4 | 1480 | 5920 | 100 | CVC4; Vampire 4.3; z3-4.7.1n; Alt-Ergo |
| CVC4; Vampire 4.3; z3-4.7.1n; Alt-Ergo | |||||
| BV | 4 | 5751 | 23004 | 100 | CVC4; Boolector; z3-4.7.1n; Q3B |
| CVC4; Boolector; z3-4.7.1n; Q3B | |||||
| BVFP | 1 | 24 | 24 | 100 | CVC4 |
| CVC4 | |||||
| FP | 1 | 61 | 61 | 100 | CVC4 |
| CVC4 | |||||
| LIA | 4 | 388 | 1552 | 100 | z3-4.7.1n; CVC4; Vampire 4.3; veriT |
| z3-4.7.1n; CVC4; Vampire 4.3; veriT | |||||
| LRA | 3 | 2419 | 7257 | 100 | z3-4.7.1n; CVC4; Vampire 4.3 |
| z3-4.7.1n; CVC4; Vampire 4.3 | |||||
| NIA | 3 | 14 | 42 | 100 | z3-4.7.1n; CVC4; Vampire 4.3 |
| z3-4.7.1n; CVC4; Vampire 4.3 | |||||
| NRA | 3 | 3813 | 11439 | 100 | z3-4.7.1n; Vampire 4.3; CVC4 |
| Vampire 4.3; z3-4.7.1n; CVC4 | |||||
| QF_ABV | 5 | 15066 | 75330 | 100 | Boolector; Yices 2.6.0; z3-4.7.1n; CVC4; MathSATn |
| Boolector; Yices 2.6.0; z3-4.7.1n; CVC4; MathSATn | |||||
| QF_ABVFP | 2 | 18129 | 36258 | 100 | CVC4; COLIBRI |
| CVC4; COLIBRI | |||||
| QF_ALIA | 6 | 139 | 834 | 100 | Yices 2.6.0; SMTInterpol; CVC4; z3-4.7.1n; veriT; MathSATn |
| Yices 2.6.0; SMTInterpol; CVC4; z3-4.7.1n; veriT; MathSATn | |||||
| QF_ANIA | 2 | 8 | 16 | 100 | z3-4.7.1n; CVC4 |
| z3-4.7.1n; CVC4 | |||||
| QF_AUFBV | 5 | 31 | 155 | 100 | CVC4; Yices 2.6.0; Boolector; z3-4.7.1n; MathSATn |
| CVC4; Yices 2.6.0; z3-4.7.1n; Boolector; MathSATn | |||||
| QF_AUFLIA | 6 | 1009 | 6054 | 100 | Yices 2.6.0; z3-4.7.1n; SMTInterpol; CVC4; veriT; MathSATn |
| Yices 2.6.0; z3-4.7.1n; SMTInterpol; CVC4; veriT; MathSATn | |||||
| QF_AUFNIA | 2 | 17 | 34 | 100 | z3-4.7.1n; CVC4 |
| z3-4.7.1n; CVC4 | |||||
| QF_AX | 5 | 551 | 2755 | 100 | Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn |
| Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn | |||||
| QF_BV | 10 | 40102 | 401020 | 100 | Boolector; Minkeyrink-ST; CVC4; STP-CMS-st-2018; Minkeyrink-MT; STP-Riss-st-2018; STP-CMS-mt-2018; z3-4.7.1n; Yices 2.6.0; MathSATn |
| Minkeyrink-MT; Boolector; Minkeyrink-ST; STP-CMS-mt-2018; CVC4; STP-CMS-st-2018; STP-Riss-st-2018; z3-4.7.1n; Yices 2.6.0; MathSATn | |||||
| QF_BVFP | 3 | 17215 | 51645 | 100 | CVC4; z3-4.7.1n; COLIBRI |
| CVC4; z3-4.7.1n; COLIBRI | |||||
| QF_DT | 2 | 8000 | 16000 | 100 | CVC4; z3-4.7.1n |
| CVC4; z3-4.7.1n | |||||
| QF_FP | 3 | 40300 | 120900 | 100 | COLIBRI; CVC4; z3-4.7.1n |
| COLIBRI; CVC4; z3-4.7.1n | |||||
| QF_IDL | 8 | 2193 | 17544 | 100 | Yices 2.6.0; z3-4.7.1n; CVC4; veriT; SMTInterpol; MathSATn; SMTRAT-Rat; CVC4-experimental-idl-2 |
| Yices 2.6.0; z3-4.7.1n; CVC4; veriT; SMTInterpol; MathSATn; SMTRAT-Rat; CVC4-experimental-idl-2 | |||||
| QF_LIA | 9 | 6947 | 62523 | 100 | SPASS-SATT; Ctrl-Ergo; MathSATn; SMTInterpol; CVC4; Yices 2.6.0; z3-4.7.1n; SMTRAT-Rat; veriT |
| SPASS-SATT; Ctrl-Ergo; MathSATn; SMTInterpol; CVC4; Yices 2.6.0; z3-4.7.1n; SMTRAT-Rat; veriT | |||||
| QF_LIRA | 5 | 7 | 35 | 100 | z3-4.7.1n; Yices 2.6.0; CVC4; SMTRAT-Rat; SMTInterpol |
| z3-4.7.1n; Yices 2.6.0; CVC4; SMTRAT-Rat; SMTInterpol | |||||
| QF_LRA | 11 | 1649 | 18139 | 100 | CVC4; SPASS-SATT; Yices 2.6.0; veriT; SMTInterpol; MathSATn; z3-4.7.1n; opensmt2; Ctrl-Ergo; SMTRAT-Rat; SMTRAT-MCSAT |
| CVC4; SPASS-SATT; Yices 2.6.0; veriT; SMTInterpol; MathSATn; z3-4.7.1n; opensmt2; Ctrl-Ergo; SMTRAT-Rat; SMTRAT-MCSAT | |||||
| QF_NIA | 5 | 23876 | 119380 | 100 | CVC4; Yices 2.6.0; z3-4.7.1n; AProVE; SMTRAT-Rat |
| CVC4; Yices 2.6.0; z3-4.7.1n; AProVE; SMTRAT-Rat | |||||
| QF_NIRA | 4 | 3 | 12 | 100 | SMTRAT-Rat; z3-4.7.1n; CVC4; Yices 2.6.0 |
| SMTRAT-Rat; z3-4.7.1n; CVC4; Yices 2.6.0 | |||||
| QF_NRA | 6 | 11489 | 68934 | 100 | z3-4.7.1n; Yices 2.6.0; veriT+raSAT+Reduce; SMTRAT-MCSAT; CVC4; SMTRAT-Rat |
| z3-4.7.1n; Yices 2.6.0; veriT+raSAT+Reduce; SMTRAT-MCSAT; CVC4; SMTRAT-Rat | |||||
| QF_RDL | 8 | 255 | 2040 | 100 | Yices 2.6.0; CVC4; z3-4.7.1n; veriT; MathSATn; SMTInterpol; opensmt2; SMTRAT-Rat |
| Yices 2.6.0; CVC4; z3-4.7.1n; veriT; MathSATn; SMTInterpol; opensmt2; SMTRAT-Rat | |||||
| QF_SLIA | 1 | 72705 | 72705 | 100 | CVC4 |
| CVC4 | |||||
| QF_UF | 7 | 7423 | 51961 | 100 | Yices 2.6.0; veriT; CVC4; z3-4.7.1n; SMTInterpol; MathSATn; opensmt2 |
| Yices 2.6.0; veriT; CVC4; z3-4.7.1n; SMTInterpol; MathSATn; opensmt2 | |||||
| QF_UFBV | 5 | 1224 | 6120 | 100 | Boolector; CVC4; Yices 2.6.0; MathSATn; z3-4.7.1n |
| Boolector; CVC4; Yices 2.6.0; MathSATn; z3-4.7.1n | |||||
| QF_UFIDL | 6 | 428 | 2568 | 100 | Yices 2.6.0; z3-4.7.1n; SMTInterpol; MathSATn; veriT; CVC4 |
| Yices 2.6.0; z3-4.7.1n; SMTInterpol; MathSATn; veriT; CVC4 | |||||
| QF_UFLIA | 6 | 583 | 3498 | 100 | Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn; veriT |
| Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn; veriT | |||||
| QF_UFLRA | 6 | 1284 | 7704 | 100 | Yices 2.6.0; MathSATn; veriT; CVC4; SMTInterpol; z3-4.7.1n |
| Yices 2.6.0; MathSATn; veriT; CVC4; SMTInterpol; z3-4.7.1n | |||||
| QF_UFNIA | 3 | 7 | 21 | 100 | Yices 2.6.0; CVC4; z3-4.7.1n |
| Yices 2.6.0; CVC4; z3-4.7.1n | |||||
| QF_UFNRA | 4 | 36 | 144 | 100 | Yices 2.6.0; z3-4.7.1n; CVC4; veriT+raSAT+Reduce |
| Yices 2.6.0; z3-4.7.1n; CVC4; veriT+raSAT+Reduce | |||||
| UF | 4 | 7562 | 30248 | 100 | CVC4; Vampire 4.3; veriT; z3-4.7.1n |
| Vampire 4.3; CVC4; veriT; z3-4.7.1n | |||||
| UFBV | 2 | 200 | 400 | 100 | z3-4.7.1n; CVC4 |
| z3-4.7.1n; CVC4 | |||||
| UFDT | 2 | 4527 | 9054 | 100 | CVC4; Vampire 4.3 |
| CVC4; Vampire 4.3 | |||||
| UFDTLIA | 2 | 303 | 606 | 100 | CVC4; Vampire 4.3 |
| CVC4; Vampire 4.3 | |||||
| UFIDL | 4 | 68 | 272 | 100 | z3-4.7.1n; CVC4; veriT; Vampire 4.3 |
| z3-4.7.1n; CVC4; veriT; Vampire 4.3 | |||||
| UFLIA | 4 | 10137 | 40548 | 100 | CVC4; veriT; z3-4.7.1n; Vampire 4.3 |
| CVC4; Vampire 4.3; veriT; z3-4.7.1n | |||||
| UFLRA | 4 | 15 | 60 | 100 | z3-4.7.1n; CVC4; veriT; Vampire 4.3 |
| z3-4.7.1n; CVC4; veriT; Vampire 4.3 | |||||
| UFNIA | 3 | 3308 | 9924 | 100 | z3-4.7.1n; Vampire 4.3; CVC4 |
| Vampire 4.3; z3-4.7.1n; CVC4 | |||||
n. Non-competing.
| Home | • | Rules | • | Benchmarks | • | Tools | • | Specs | • | Participants | • | Results | • | SMT-LIB | • | Previous |
|---|
Last modified: Fri 13 Jul 2018 00:05 UTC