diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3270c1c07..3e59aebe6 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -357,8 +357,10 @@ TrustNode TheoryArrays::ppRewrite(TNode term) return TrustNode::null(); } - -Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheoryArrays::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) +{ + TNode in = tin.getNode(); switch(in.getKind()) { case kind::EQUAL: { @@ -366,12 +368,12 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs d_ppEqualityEngine.assertEquality(in, true, in); if (in[0].isVar() && isLegalElimination(in[0], in[1])) { - outSubstitutions.addSubstitution(in[0], in[1]); + outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); return PP_ASSERT_STATUS_SOLVED; } if (in[1].isVar() && isLegalElimination(in[1], in[0])) { - outSubstitutions.addSubstitution(in[1], in[0]); + outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); return PP_ASSERT_STATUS_SOLVED; } break; |