The International Satisfiability Modulo Theories (SMT) Competition.


SMT-COMP 2020 Alternative

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 divisions

Quantified divisions


The divisions above were determined following:

  1. Similar logics that do not standout by themselves were combined
  2. 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.
  3. Arrays and datatypes are handled in a similar enough way to UF to be combined with it.
  4. Floating-point logics are combined since generally this is the dominating component for any logic contaning FP.