diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7d6f27aa5..39eaf5b95 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -127,6 +127,7 @@ void Smt2::setLogic(const std::string& name) { case Smt::QF_UFIDL: case Smt::QF_UFLIA: + case Smt::QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addOperator(kind::APPLY_UF); break; @@ -137,6 +138,13 @@ void Smt2::setLogic(const std::string& name) { addOperator(kind::APPLY_UF); break; + case Smt::QF_UFLIRA:// nonstandard logic + case Smt::QF_UFNIRA:// nonstandard logic + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + break; + case Smt::QF_BV: addTheory(THEORY_BITVECTORS); break; |