The International Satisfiability Modulo Theories (SMT) Competition.

This website contains the results of SMT-COMP 2020 Single Query if the same solvers had entered but the logics were combined into the following divisions:

- QF_Equality
- Logics: QF_UF, QF_AX, QF_DT

- QF_Equality+LinearArith
- Logics: QF_ALIA, QF_AUFLIA, QF_UFLIA, QF_UFLRA, QF_UFIDL

- QF_Equality+NonLinearArith
- Logics: QF_UFNRA, QF_UFNIA, QF_ANIA, QF_AUFNIA

- QF_Equality+BVArith
- Logics: QF_ABV, QF_UFBV, QF_AUFBV

- QF_LinearIntArith
- Logics: QF_LIA, QF_LIRA, QF_IDL

- QF_LinearRealArith
- Logics: QF_LRA, QF_RDL

- QF_BV
- QF_FPArith
- Logics: QF_FP, QF_UFFP, QF_FPLRA, QF_BVFP, QF_ABVFP, QF_BVFPLRA, QF_ABVFPLRA

- QF_NonLinearIntArith
- Logics: QF_NIA, QF_NIRA

- QF_NRA
- QF_Strings
- Logics: QF_S, QF_SLIA

- Equality
- Logics: UF, UFDT

- Equality+LinearArith
- Logics: ALIA, AUFLIA, UFLIA, UFIDL, AUFLIRA, UFLRA, UFDTLIA, UFDTLIRA, AUFDTLIA, AUFDTLIRA

- Equality+MachineArith
- Logics: AUFFPDTLIRA, UFFPDTLIRA, UFFPDTNIRA, ABVFP, ABVFPLRA, UFBV, AUFBVDTLIA

- Equality+NonLinearArith
- Logics: AUFDTNIRA, UFDTNIA, UFDTNIRA, AUFNIA, AUFNIRA, UFNIA

- Arith
- Logics: LRA, LIA, NIA, NRA

- BV
- FPArith
- Logics: BVFP, FP, BVFPLRA, FPLRA

The divisions above were determined following:

- Similar logics that do not standout by themselves were combined
- Integer and real, as well as bit-vector and floating-point, arithmetics are separated
- note that the “Arith” division goes against this however its composing logics do not standout out by themselves as currently represented in SMT-LIB.

- Arrays and datatypes are handled in a similar enough way to UF to be combined with it.
- Floating-point logics are combined since generally this is the dominating component for any logic contaning FP.