diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-07 17:35:21 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-07 17:35:21 -0400 |
| commit | 5ab1e41905c94275896dce77da592d3de329e712 (patch) | |
| tree | 394d07af4db4d4815fd8c5cede475a13591ba492 /src/smt | |
| parent | 0d8c1936b8b8159af5f6688e63d74a806f48ac75 (diff) | |
One more case for arrays of Boolean.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/boolean_terms.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index ffd17dc07..b3e69619f 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -507,7 +507,19 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa result.top() << n; worklist.pop(); goto next_worklist; - } else if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) { + } else if(indexType == t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) { + TypeNode newType = nm->mkArrayType(indexType, constituentType); + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", + newType, "an array variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + top.setAttribute(BooleanTermAttr(), n); + Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; + d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); + d_termCache[make_pair(top, parentTheory)] = n; + result.top() << n; + worklist.pop(); + goto next_worklist; + } else if(indexType != t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) { TypeNode newType = nm->mkArrayType(indexType, constituentType); Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", newType, "an array variable introduced by Boolean-term conversion", |