The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Page generated on 2020-07-04 11:47:01 +0000
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| CVC4 | 375.0 | 0.00577886 | AUFBVDTLIA |
| CVC4 | 327.0 | 0.10145009 | UFFPDTLIRA |
| CVC4 | 116.0 | 19.80994196 | AUFFPDTLIRA |
| CVC4 | 93.0 | 0.00921732 | BVFPLRA |
| CVC4 | 19.0 | 0.0148046 | ABVFPLRA |
| CVC4 | 16.0 | 0.00677667 | FPLRA |
| CVC4 | 15.0 | 0.86442915 | QF_ANIA |
| CVC4 | 8.0 | 0.00949594 | UFFPDTNIRA |
| CVC4 | 5.0 | 19.61071998 | QF_DT |
| CVC4 | 4.45098039 | 0.01263987 | FP |
| CVC4 | 4.07142857 | 0.05144108 | BVFP |
| CVC4 | 4.0 | 0.13723384 | UFBV |
| CVC4 | 2.69090909 | 4.86800827 | AUFDTLIA |
| CVC4 | 2.68859649 | 0.93519849 | BV |
| Yices2 | 2.0 | 1.78582208 | QF_UFNRA |
| CVC4 | 1.84259259 | 1858.41425687 | LIA |
| Yices2 | 1.73333333 | 0.35695797 | QF_AUFBV |
| CVC4 | 1.60068847 | 1.55472084 | UFNIA |
| CVC4 | 1.54330709 | 1.2473082 | UFDTLIA |
| SMT-RAT | 1.5 | 4.70278035 | QF_NIRA |
| CVC4 | 1.45454545 | 0.00754356 | ABVFP |
| CVC4 | 1.45172414 | 1.12927744 | UFDT |
| CVC4 | 1.44444444 | 0.02781039 | NIA |
| Vampire | 1.31746032 | 2.59119683 | NRA |
| CVC4 | 1.2950495 | 1.83705726 | LRA |
| CVC4 | 1.25 | 136.78962529 | QF_AUFNIA |
| CVC4 | 1.22222222 | 0.85192699 | UFIDL |
| COLIBRI | 1.17021277 | 3.61990836 | QF_FPLRA |
| Yices2 | 1.16666667 | 1.79263826 | QF_LIRA |
| CVC4 | 1.14270428 | 10.3110819 | QF_SLIA |
| Yices2 | 1.13162939 | 1.39365658 | QF_NRA |
| CVC4 | 1.10791367 | 0.96812628 | QF_BVFPLRA |
| Yices2 | 1.09104258 | 1.90084996 | QF_IDL |
| Bitwuzla | 1.08837209 | 1.06404719 | QF_FP |
| CVC4 | 1.06952491 | 11.38868456 | QF_S |
| SMTInterpol | 1.05263158 | 0.02693054 | ALIA |
| Yices2 | 1.04912281 | 9.97570905 | QF_UFIDL |
| CVC4 | 1.04460905 | 0.85824319 | QF_NIA |
| CVC4 | 1.0418372 | 1.28882604 | QF_LIA |
| OpenSMT | 1.03826531 | 1.87663173 | QF_LRA |
| Vampire | 1.0372093 | 0.66970109 | AUFDTNIRA |
| CVC4 | 1.03481013 | 1.06498885 | UFLIA |
| CVC4 | 1.02898551 | 0.05382805 | QF_ABVFPLRA |
| CVC4 | 1.02882663 | 27.94924656 | UFDTLIRA |
| Bitwuzla | 1.02279289 | 1.97740034 | QF_BV |
| Bitwuzla | 1.02040816 | 4.32668307 | QF_ABVFP |
| Yices2 | 1.01923077 | 0.2198779 | QF_UFBV |
| Yices2 | 1.01904762 | 1.21801051 | QF_RDL |
| CVC4 | 1.01712887 | 1.2276737 | AUFLIRA |
| CVC4 | 1.01460789 | 6.60559365 | AUFDTLIRA |
| Vampire | 1.01037344 | 1.07001685 | UF |
| CVC4 | 1.00716846 | 5.45673027 | QF_UFNIA |
| CVC4 | 1.00609756 | 4.05915034 | UFDTNIRA |
| Vampire | 1.00457457 | 0.97683559 | AUFLIA |
| Bitwuzla | 1.00357249 | 1.77170632 | QF_ABV |
| Yices2 | 1.0 | 18.48083335 | QF_AX |
| Vampire | 1.0 | 15.36977528 | UFDTNIA |
| Yices2 | 1.0 | 14.78945874 | QF_ALIA |
| Yices2 | 1.0 | 7.62415245 | QF_UFLIA |
| Yices2 | 1.0 | 6.8275957 | QF_AUFLIA |
| Bitwuzla | 1.0 | 2.1569542 | QF_BVFP |
| Yices2 | 1.0 | 2.11246098 | QF_UF |
| Alt-Ergo | 1.0 | 1.33600763 | UFLRA |
| Bitwuzla | 1.0 | 1.33102926 | QF_UFFP |
| CVC4 | 1.0 | 1.02631555 | AUFNIRA |
| Yices2 | 1.0 | 1.01649723 | QF_UFLRA |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| CVC4 | 375.0 | 0.00412019 | AUFBVDTLIA |
| CVC4 | 327.0 | 0.06945504 | UFFPDTLIRA |
| CVC4 | 116.0 | 13.68512829 | AUFFPDTLIRA |
| CVC4 | 93.0 | 0.00620038 | BVFPLRA |
| CVC4 | 19.0 | 0.00993545 | ABVFPLRA |
| CVC4 | 16.0 | 0.0047398 | FPLRA |
| CVC4 | 15.0 | 0.48066938 | QF_ANIA |
| CVC4 | 8.0 | 0.00657843 | UFFPDTNIRA |
| CVC4 | 5.0 | 19.60673848 | QF_DT |
| CVC4 | 4.45098039 | 0.00881189 | FP |
| CVC4 | 4.07142857 | 0.04501662 | BVFP |
| CVC4 | 4.0 | 0.12792546 | UFBV |
| CVC4 | 2.69090909 | 2.05708149 | AUFDTLIA |
| CVC4 | 2.68859649 | 0.90373643 | BV |
| Yices2 | 2.0 | 1.78604616 | QF_UFNRA |
| CVC4 | 1.84259259 | 1845.89798109 | LIA |
| Yices2 | 1.73333333 | 0.35708613 | QF_AUFBV |
| CVC4 | 1.53125 | 1.20008368 | UFDTLIA |
| SMT-RAT | 1.5 | 4.70444182 | QF_NIRA |
| CVC4 | 1.45454545 | 0.00533719 | ABVFP |
| CVC4 | 1.44444444 | 0.01560731 | NIA |
| Vampire | 1.35616438 | 1.446819 | AUFDTNIRA |
| Vampire | 1.31746032 | 2.62021729 | NRA |
| CVC4 | 1.29526462 | 1.39128414 | UFNIA |
| CVC4 | 1.2950495 | 1.81992445 | LRA |
| CVC4 | 1.28353659 | 1.08448595 | UFDT |
| CVC4 | 1.25 | 35.00416298 | QF_AUFNIA |
| CVC4 | 1.22222222 | 0.83269274 | UFIDL |
| COLIBRI | 1.17021277 | 3.61987015 | QF_FPLRA |
| Yices2 | 1.16666667 | 1.79315794 | QF_LIRA |
| CVC4 | 1.14270428 | 10.2589371 | QF_SLIA |
| Yices2 | 1.13162939 | 1.39369411 | QF_NRA |
| CVC4 | 1.10791367 | 0.96810708 | QF_BVFPLRA |
| Yices2 | 1.09104258 | 1.90052172 | QF_IDL |
| Bitwuzla | 1.08837209 | 1.06480769 | QF_FP |
| CVC4 | 1.06952491 | 11.36030118 | QF_S |
| SMTInterpol | 1.05263158 | 0.06601609 | ALIA |
| Yices2 | 1.04912281 | 9.32704902 | QF_UFIDL |
| Vampire | 1.0466805 | 1.12215703 | UF |
| CVC4 | 1.04477366 | 0.85275034 | QF_NIA |
| CVC4 | 1.0418372 | 1.28986491 | QF_LIA |
| OpenSMT | 1.03826531 | 1.8844866 | QF_LRA |
| CVC4 | 1.03481013 | 1.0524316 | UFLIA |
| Vampire | 1.03333333 | 1.0001937 | AUFNIRA |
| CVC4 | 1.02898551 | 0.0540611 | QF_ABVFPLRA |
| CVC4 | 1.02840909 | 26.85338184 | UFDTLIRA |
| Vampire | 1.02121212 | 0.15736061 | UFDTNIRA |
| Bitwuzla | 1.02040816 | 4.31963823 | QF_ABVFP |
| Yices2 | 1.01923077 | 0.2199016 | QF_UFBV |
| Yices2 | 1.01904762 | 1.21824877 | QF_RDL |
| CVC4 | 1.00716846 | 5.44942701 | QF_UFNIA |
| Vampire | 1.00640439 | 1.0210319 | AUFLIA |
| Bitwuzla | 1.00612855 | 1.15552005 | QF_BV |
| Bitwuzla | 1.00357249 | 1.77163892 | QF_ABV |
| CVC4 | 1.0035488 | 15.83026393 | AUFDTLIRA |
| Vampire | 1.00160385 | 0.94611938 | AUFLIRA |
| Vampire | 1.0 | 15.33573147 | UFDTNIA |
| Yices2 | 1.0 | 12.34818603 | QF_AX |
| Yices2 | 1.0 | 10.0089598 | QF_UFLIA |
| Yices2 | 1.0 | 8.25652704 | QF_ALIA |
| Yices2 | 1.0 | 5.99153801 | QF_AUFLIA |
| Bitwuzla | 1.0 | 2.13763193 | QF_BVFP |
| Yices2 | 1.0 | 2.05809455 | QF_UF |
| Alt-Ergo | 1.0 | 1.57081153 | UFLRA |
| Bitwuzla | 1.0 | 1.3480797 | QF_UFFP |
| Yices2 | 1.0 | 1.01621683 | QF_UFLRA |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| CVC4 | 153.0 | 0.00870447 | AUFBVDTLIA |
| CVC4 | 94.0 | 0.00913066 | AUFDTLIA |
| CVC4 | 88.0 | 0.03480652 | BVFPLRA |
| CVC4 | 83.0 | 0.13368853 | QF_ANIA |
| CVC4 | 70.0 | 70.84800187 | UFDTLIRA |
| CVC4 | 28.0 | 0.20233942 | UFFPDTLIRA |
| CVC4 | 17.0 | 11.70573592 | ABVFPLRA |
| CVC4 | 16.0 | 0.01713403 | FPLRA |
| CVC4 | 12.0 | 0.88152815 | BV |
| CVC4 | 6.8 | 2.46579216 | UFDT |
| CVC4 | 4.58333333 | 0.01296857 | BVFP |
| CVC4 | 4.13636364 | 1676.34709885 | LIA |
| CVC4 | 4.0 | 1.09351185 | QF_DT |
| CVC4 | 3.0 | 19.48338979 | QF_AUFNIA |
| Yices2 | 2.18181818 | 1.78558955 | QF_UFNRA |
| SMTInterpol | 2.0 | 0.90729786 | ALIA |
| Yices2 | 1.8 | 0.07907123 | QF_AUFBV |
| CVC4 | 1.5 | 0.04966083 | NIA |
| CVC4 | 1.33663366 | 2.01200147 | LRA |
| SMTInterpol | 1.33333333 | 1.09937705 | UFLIA |
| CVC4 | 1.31707317 | 2.55718648 | AUFLIA |
| CVC4 | 1.27272727 | 7.92175111 | ABVFP |
| CVC4 | 1.25 | 0.00528478 | FP |
| CVC4 | 1.24004798 | 27.52610228 | QF_SLIA |
| CVC4 | 1.1875 | 2.87761159 | QF_BVFPLRA |
| Vampire | 1.179941 | 11.69989562 | UF |
| CVC4 | 1.15104167 | 13.20192959 | QF_S |
| Yices2 | 1.14858491 | 3.44106774 | QF_IDL |
| COLIBRI | 1.13953488 | 2.96783769 | QF_FPLRA |
| Bitwuzla | 1.13333333 | 2.72015318 | QF_FP |
| CVC4 | 1.12733072 | 0.85283897 | QF_NIA |
| CVC4 | 1.1237721 | 0.84627468 | UFNIA |
| Yices2 | 1.08643617 | 1.2429135 | QF_NRA |
| CVC4 | 1.06345178 | 1.43098692 | QF_LIA |
| Bitwuzla | 1.04444444 | 23.18147049 | QF_ABVFP |
| Yices2 | 1.02912621 | 13.50507232 | QF_RDL |
| Yices2 | 1.02475248 | 1.34900678 | QF_UFNIA |
| OpenSMT | 1.02380952 | 1.16957952 | QF_LRA |
| CVC4 | 1.01470588 | 0.0694678 | QF_ABVFPLRA |
| Bitwuzla | 1.00998403 | 1.37599959 | QF_BV |
| Yices2 | 1.00775194 | 0.62022225 | QF_UFBV |
| Bitwuzla | 1.00260191 | 2.32820613 | QF_ABV |
| Yices2 | 1.0 | 21.87330851 | QF_UFLIA |
| Yices2 | 1.0 | 11.49759442 | QF_AUFLIA |
| Bitwuzla | 1.0 | 5.21787286 | QF_BVFP |
| Yices2 | 1.0 | 3.36830933 | QF_ALIA |
| Yices2 | 1.0 | 3.05218467 | QF_AX |
| Yices2 | 1.0 | 2.24731887 | QF_UFIDL |
| CVC4 | 1.0 | 2.10728865 | UFIDL |
| Yices2 | 1.0 | 2.03423307 | QF_UF |
| Yices2 | 1.0 | 1.99712199 | QF_LIRA |
| Yices2 | 1.0 | 1.03064541 | QF_UFLRA |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| CVC4 | 300.0 | 1.62797292 | UFFPDTLIRA |
| CVC4 | 223.0 | 0.04157801 | AUFBVDTLIA |
| CVC4 | 116.0 | 13.33108223 | AUFFPDTLIRA |
| CVC4 | 8.0 | 2.65244868 | UFFPDTNIRA |
| CVC4 | 6.0 | 1.19566055 | BVFPLRA |
| CVC4 | 4.6971831 | 0.01821126 | FP |
| CVC4 | 4.0 | 0.01397398 | UFBV |
| CVC4 | 3.0 | 4.38858477 | ABVFP |
| CVC4 | 3.0 | 1.05164331 | ABVFPLRA |
| Vampire | 2.5 | 0.01167528 | NIA |
| CVC4 | 2.0744186 | 1.11216821 | BV |
| CVC4 | 2.0 | 19.62014357 | QF_DT |
| Yices2 | 1.63636364 | 0.01244403 | QF_AUFBV |
| CVC4 | 1.53125 | 1.48827467 | UFDTLIA |
| SMT-RAT | 1.5 | 4.70444182 | QF_NIRA |
| CVC4 | 1.5 | 0.03009535 | QF_ABVFPLRA |
| COLIBRI | 1.4 | 105.40632499 | QF_FPLRA |
| Vampire | 1.35616438 | 1.446819 | AUFDTNIRA |
| CVC4 | 1.33333333 | 1.74130742 | QF_ANIA |
| Vampire | 1.31746032 | 2.97665841 | NRA |
| CVC4 | 1.26644737 | 1.80377235 | LRA |
| CVC4 | 1.25 | 983.94043215 | UFIDL |
| Yices2 | 1.2 | 1.79240454 | QF_LIRA |
| Yices2 | 1.14090131 | 1.90522996 | QF_NIA |
| Vampire | 1.11237323 | 0.12140189 | UFDTLIRA |
| CVC4 | 1.09589041 | 15.86263163 | QF_UFNIA |
| CVC4 | 1.09 | 1605.33840897 | LIA |
| COLIBRI | 1.07317073 | 2.20376644 | QF_BVFPLRA |
| Yices2 | 1.06603774 | 9.30643059 | QF_UFIDL |
| CVC4 | 1.04874652 | 1.32497584 | UFNIA |
| SMTInterpol | 1.03768116 | 1.33408415 | QF_LIA |
| Yices2 | 1.0375 | 0.21418978 | QF_UFBV |
| Vampire | 1.03346856 | 3.35035268 | AUFLIA |
| Vampire | 1.03333333 | 1.39877559 | AUFNIRA |
| CVC4 | 1.03322785 | 1.44845865 | UFLIA |
| OpenSMT | 1.02659574 | 1.80738638 | QF_LRA |
| CVC4 | 1.02622951 | 1.29167157 | UF |
| Vampire | 1.02121212 | 0.159012 | UFDTNIRA |
| CVC4 | 1.01910828 | 1.235138 | UFDT |
| Bitwuzla | 1.01496259 | 4.11167842 | QF_ABVFP |
| Yices2 | 1.01380042 | 1.15835973 | QF_NRA |
| CVC4 | 1.01316708 | 4.2751006 | QF_SLIA |
| Bitwuzla | 1.01020408 | 0.66297826 | QF_FP |
| Yices2 | 1.00925926 | 1.97071507 | QF_RDL |
| Bitwuzla | 1.0056926 | 1.63566886 | QF_ABV |
| CVC4 | 1.00416667 | 227.48481727 | QF_S |
| CVC4 | 1.00389105 | 0.90778825 | QF_IDL |
| Bitwuzla | 1.00382135 | 1.03379156 | QF_BV |
| CVC4 | 1.0035488 | 17.0536606 | AUFDTLIRA |
| Vampire | 1.00160385 | 0.61119085 | AUFLIRA |
| Yices2 | 1.0 | 45.36970439 | QF_ALIA |
| CVC4 | 1.0 | 36.57032982 | QF_AUFNIA |
| CVC4 | 1.0 | 25.40874081 | AUFDTLIA |
| Yices2 | 1.0 | 17.29193886 | QF_AX |
| Vampire | 1.0 | 15.33573147 | UFDTNIA |
| Yices2 | 1.0 | 8.39063267 | QF_UFLIA |
| CVC4 | 1.0 | 5.32788929 | BVFP |
| Yices2 | 1.0 | 4.06876603 | QF_UFNRA |
| Yices2 | 1.0 | 3.20415766 | QF_AUFLIA |
| Yices2 | 1.0 | 2.05871132 | QF_UF |
| Bitwuzla | 1.0 | 1.3480797 | QF_UFFP |
| CVC4 | 1.0 | 1.33800512 | ALIA |
| Bitwuzla | 1.0 | 1.33581085 | QF_BVFP |
| Yices2 | 1.0 | 1.24212119 | QF_UFLRA |
| veriT | 1.0 | 1.0045895 | UFLRA |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| CVC4 | 321.0 | 1.32270012 | UFFPDTLIRA |
| CVC4 | 194.0 | 0.13990968 | AUFBVDTLIA |
| CVC4 | 116.0 | 13.68512829 | AUFFPDTLIRA |
| CVC4 | 93.0 | 0.30183632 | BVFPLRA |
| CVC4 | 20.5 | 0.85057692 | QF_ANIA |
| CVC4 | 19.0 | 0.45393783 | ABVFPLRA |
| CVC4 | 14.0 | 0.20660907 | FPLRA |
| CVC4 | 8.0 | 0.3093457 | UFFPDTNIRA |
| CVC4 | 5.0 | 8.29729293 | QF_AUFNIA |
| CVC4 | 4.07142857 | 0.65568673 | BVFP |
| CVC4 | 4.0130719 | 0.30048213 | FP |
| CVC4 | 4.0 | 1.00391742 | QF_DT |
| Vampire | 3.67741935 | 1.07295203 | UFDTLIA |
| CVC4 | 2.33480176 | 0.90256142 | BV |
| CVC4 | 2.28571429 | 0.27735302 | UFBV |
| CVC4 | 2.0 | 2.06917603 | AUFDTLIA |
| CVC4 | 1.8608838 | 1.37342677 | UFNIA |
| CVC4 | 1.85981308 | 56.05002462 | LIA |
| Yices2 | 1.54545455 | 0.41986455 | QF_AUFBV |
| Vampire | 1.53875969 | 1.15115625 | UF |
| Yices2 | 1.51961342 | 1.45359794 | QF_NIA |
| Yices2 | 1.5 | 1.05901556 | QF_UFNRA |
| Yices2 | 1.49776786 | 2.22921469 | QF_IDL |
| CVC4 | 1.45454545 | 0.2486232 | ABVFP |
| CVC4 | 1.30263158 | 1.87299885 | LRA |
| Vampire | 1.3 | 1.01830517 | AUFNIRA |
| Vampire | 1.26984127 | 2.09814063 | NRA |
| COLIBRI | 1.22222222 | 2.1946038 | QF_FPLRA |
| CVC4 | 1.22222222 | 0.39289897 | NIA |
| COLIBRI | 1.18072289 | 1.35201555 | QF_FP |
| Yices2 | 1.15283541 | 1.43837036 | QF_NRA |
| Yices2 | 1.14460512 | 1.94611397 | QF_LIA |
| Yices2 | 1.13513514 | 5.75988662 | QF_UFIDL |
| Yices2 | 1.12941176 | 1.3850074 | QF_RDL |
| CVC4 | 1.12184874 | 3.12262622 | QF_SLIA |
| CVC4 | 1.11111111 | 1.0862062 | UFIDL |
| CVC4 | 1.10877863 | 1.13510348 | UFLIA |
| Vampire | 1.10758197 | 1.3457193 | AUFLIA |
| Bitwuzla | 1.05856833 | 2.57394811 | QF_ABVFP |
| CVC4 | 1.05471478 | 2.01885609 | QF_S |
| Yices2 | 1.05405405 | 5.70174813 | QF_ALIA |
| Bitwuzla | 1.05291005 | 1.29665472 | QF_UFBV |
| SMTInterpol | 1.05263158 | 0.06601609 | ALIA |
| Alt-Ergo | 1.0390625 | 1.07238014 | UFDT |
| CVC4 | 1.03623188 | 0.87795636 | QF_BVFPLRA |
| CVC4 | 1.02955665 | 2.65055481 | AUFDTNIRA |
| CVC4 | 1.02941176 | 3.59070569 | QF_UFNIA |
| CVC4 | 1.02882663 | 15.84833309 | UFDTLIRA |
| CVC4 | 1.02753962 | 6.31996804 | AUFDTLIRA |
| Yices2 | 1.01960784 | 1.11093693 | QF_LRA |
| Bitwuzla | 1.0177544 | 0.91404579 | QF_BV |
| Yices2 | 1.01689189 | 6.11634482 | QF_UFLIA |
| CVC4 | 1.01538462 | 3.934404 | UFDTNIRA |
| Vampire | 1.01334445 | 1.0204656 | AUFLIRA |
| Bitwuzla | 1.00822168 | 1.21699993 | QF_ABV |
| Bitwuzla | 1.00779221 | 1.95168186 | QF_BVFP |
| Vampire | 1.0 | 15.33573147 | UFDTNIA |
| Yices2 | 1.0 | 12.34818603 | QF_AX |
| Yices2 | 1.0 | 5.99153801 | QF_AUFLIA |
| COLIBRI | 1.0 | 1.61450804 | QF_ABVFPLRA |
| Yices2 | 1.0 | 1.46094919 | QF_UFLRA |
| Yices2 | 1.0 | 1.36229846 | QF_UF |
| Bitwuzla | 1.0 | 1.3480797 | QF_UFFP |
| Yices2 | 1.0 | 1.12333685 | QF_LIRA |
| Alt-Ergo | 1.0 | 1.011224 | UFLRA |
n Non-competing.
e Experimental.