diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e86a09112..f8694e760 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -980,7 +980,13 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa void TheoryEngine::preprocessStart() { d_tpp.clearCache(); } Node TheoryEngine::preprocess(TNode assertion) { - return d_tpp.theoryPreprocess(assertion); + TrustNode trn = d_tpp.theoryPreprocess(assertion); + if (trn.isNull()) + { + // no change + return assertion; + } + return trn.getNode(); } void TheoryEngine::notifyPreprocessedAssertions( @@ -1633,6 +1639,12 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, std::vector<Node> newSkolems; TrustNode tlemma = d_tpp.preprocess(node, newLemmas, newSkolems, preprocess); + // !!!!!!! temporary, until this method is fully updated from proof-new + if (tlemma.isNull()) + { + tlemma = TrustNode::mkTrustLemma(node); + } + // must use an assertion pipeline due to decision engine below AssertionPipeline lemmas; // make the assertion pipeline |