2 files changed, 16 insertions, 1 deletions
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index e0d1922c8..0ee6944d4 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -41,6 +41,8 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFIDL"] = QF_UFIDL;
   logicMap["QF_UFLRA"] = QF_UFLRA;
   logicMap["QF_UFLIA"] = QF_UFLIA;
+  logicMap["QF_AUFLIA"] = QF_AUFLIA;
+  logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
   return logicMap;
 }
 
@@ -175,13 +177,25 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case QF_AUFLIA:
+    addTheory(THEORY_ARRAYS_EX);
+    addUf();
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_AUFLIRA:
+    addTheory(THEORY_ARRAYS_EX);
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    break;
+
   case AUFLIA:
   case AUFLIRA:
   case AUFNIRA:
   case LRA:
   case UFNIA:
   case QF_AUFBV:
-  case QF_AUFLIA:
     Unhandled(name);
   }
 }
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 11a30c2fc..a99f81998 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -42,6 +42,7 @@ public:
     LRA,
     QF_AUFBV,
     QF_AUFLIA,
+    QF_AUFLIRA,
     QF_AX,
     QF_BV,
     QF_IDL,