From 5ab1e41905c94275896dce77da592d3de329e712 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Jun 2013 17:35:21 -0400 Subject: [PATCH] One more case for arrays of Boolean. --- src/smt/boolean_terms.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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", -- 2.30.2