diff options
-rw-r--r-- | src/parser/smt/smt.cpp | 6 |
1 files 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); |