From d81e163d8d8351fce8a26f3f9e8a6303fbf1358a Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Thu, 8 Jul 2010 19:12:32 +0000
Subject: [PATCH] Fixing Array type in SMT v1.2

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

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);
-- 
2.30.2