Fixing Array type in SMT v1.2

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index bb592857aee9c3472e1b745c989c32f79ffeca6b..fe7d774550632ae5e055a31a7ed33d66a344f0a0 100644 (file)
--- 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);