diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-05-15 18:22:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-05-15 18:22:14 +0000 |
commit | 23b6734f73022ee86d37315134821fb52c1727d1 (patch) | |
tree | 330f3ca69dfa9a243e57bfb7312bc19f623a6276 /src/parser/smt | |
parent | 174f9a65685b0268b20d42fc0ebbcd46ae98c905 (diff) |
Fix QF_AUFLIA (resolves bug #331).
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/smt.cpp | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index edba64b7a..ade887b23 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -98,7 +98,15 @@ void Smt::addTheory(Theory theory) { seq->addCommand(new DeclareTypeCommand("Element", 0, elementType)); preemptCommand(seq); - defineType("Array", getExprManager()->mkArrayType(indexType,elementType)); + defineType("Array", getExprManager()->mkArrayType(indexType, elementType)); + + addOperator(kind::SELECT); + addOperator(kind::STORE); + break; + } + + case THEORY_INT_ARRAYS_EX: { + defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType())); addOperator(kind::SELECT); addOperator(kind::STORE); @@ -212,7 +220,7 @@ void Smt::setLogic(const std::string& name) { break; case QF_AUFLIA: - addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_INT_ARRAYS_EX); addUf(); addTheory(THEORY_INTS); break; |