diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9e69c9f71..93eadde43 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -296,7 +296,19 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems) { - // first, see if we need to expand definitions + // first, check for logic exceptions + Kind k = term.getKind(); + if (!options().arrays.arraysExp) + { + if (k == kind::EQ_RANGE) + { + std::stringstream ss; + ss << "Term of kind " << k + << " not supported in default mode, try --arrays-exp"; + throw LogicException(ss.str()); + } + } + // see if we need to expand definitions TrustNode texp = d_rewriter.expandDefinition(term); if (!texp.isNull()) { @@ -309,7 +321,8 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems) d_ppEqualityEngine.addTerm(term); NodeManager* nm = NodeManager::currentNM(); Node ret; - switch (term.getKind()) { + switch (k) + { case kind::SELECT: { // select(store(a,i,v),j) = select(a,j) // IF i != j |