Fix QF_AUFLIA (resolves bug #331).

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index edba64b7af5c55677735f139ba2e7823ad7dba8f..ade887b23ec0e0bb7c0c92bf67df59b364927c11 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -98,7 +98,15 @@ void Smt::addTheory(Theory theory) {
     seq->addCommand(new DeclareTypeCommand("Element", 0, elementType));
     preemptCommand(seq);
 
-    defineType("Array", getExprManager()->mkArrayType(indexType,elementType));
+    defineType("Array", getExprManager()->mkArrayType(indexType, elementType));
+
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_INT_ARRAYS_EX: {
+    defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
 
     addOperator(kind::SELECT);
     addOperator(kind::STORE);
@@ -212,7 +220,7 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case QF_AUFLIA:
-    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_INT_ARRAYS_EX);
     addUf();
     addTheory(THEORY_INTS);
     break;