add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT inputs, for testing

1 files changed, 13 insertions, 1 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 08a824c0a..7d6f27aa5 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -141,13 +141,25 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case Smt::QF_AUFLIA:
+    addTheory(THEORY_ARRAYS);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    break;
+
+  case Smt::QF_AUFLIRA:
+    addTheory(THEORY_ARRAYS);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    break;
+
   case Smt::AUFLIA:
   case Smt::AUFLIRA:
   case Smt::AUFNIRA:
   case Smt::LRA:
   case Smt::UFNIA:
   case Smt::QF_AUFBV:
-  case Smt::QF_AUFLIA:
     Unhandled(name);
   }
 }