diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-08 19:12:32 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-08 19:12:32 +0000 |
| commit | d81e163d8d8351fce8a26f3f9e8a6303fbf1358a (patch) | |
| tree | 76f79ed8432915f3f8b67b07fb53da0dba20522f /src/parser/smt | |
| parent | 02338930d0e92190c7c27a350a527db2c1b5c040 (diff) | |
Fixing Array type in SMT v1.2
Diffstat (limited to 'src/parser/smt')
| -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); |