diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 34245669e..79d5ccb3a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -128,17 +128,27 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_REALS); break; + case Smt::QF_UF: + addOperator(kind::APPLY_UF); + break; + case Smt::QF_UFIDL: addTheory(THEORY_INTS); - // falling-through on purpose, to add UF part of UFIDL + addOperator(kind::APPLY_UF); + break; - case Smt::QF_UF: + case Smt::QF_UFLIA: + case Smt::QF_UFLRA: + case Smt::QF_UFNRA: + addTheory(THEORY_REALS); addOperator(kind::APPLY_UF); break; case Smt::AUFLIA: case Smt::AUFLIRA: case Smt::AUFNIRA: + case Smt::LRA: + case Smt::UFNIA: case Smt::QF_AUFBV: case Smt::QF_AUFLIA: case Smt::QF_BV: |