From 23b6734f73022ee86d37315134821fb52c1727d1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 15 May 2012 18:22:14 +0000
Subject: Fix QF_AUFLIA (resolves bug #331).

---
 src/parser/smt/smt.cpp | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index edba64b7a..ade887b23 100644
--- 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;
-- 
cgit v1.2.3