From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 15 May 2012 18:22:14 +0000 (+0000)
Subject: Fix QF_AUFLIA (resolves bug #331).
X-Git-Tag: cvc5-1.0.0~8177
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=23b6734f73022ee86d37315134821fb52c1727d1;p=cvc5.git

Fix QF_AUFLIA (resolves bug #331).
---

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;