From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 8 Jul 2010 19:12:32 +0000 (+0000)
Subject: Fixing Array type in SMT v1.2
X-Git-Tag: cvc5-1.0.0~8914
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d81e163d8d8351fce8a26f3f9e8a6303fbf1358a;p=cvc5.git

Fixing Array type in SMT v1.2
---

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index bb592857a..fe7d77455 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -83,11 +83,9 @@ void Smt::addTheory(Theory theory) {
   case THEORY_ARRAYS:
   case THEORY_ARRAYS_EX: {
     Type indexType = mkSort("Index");
-    Type elementTYpe = mkSort("Element");
+    Type elementType = mkSort("Element");
     
-    // FIXME: should be defineType("Array",arrayType(indexType,elementType))
-    // but arrayType isn't defined
-    mkSort("Array");
+    defineType("Array",getExprManager()->mkArrayType(indexType,elementType));
 
     addOperator(kind::SELECT);
     addOperator(kind::STORE);