SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Biggest Lead Ranking- Single Query Track

Page generated on 2020-07-04 11:47:01 +0000

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
CVC4 CVC4 CVC4 CVC4 CVC4

Sequential Performance

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

Parallel Performance

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

SAT Performance

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

UNSAT Performance

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

24s Performance

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.