diff options
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 77ee1effd..184584aa9 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -68,7 +68,7 @@ bool ProofEqEngine::assertFact(Node lit, ps.d_args = args; d_factPg.addStep(lit, ps); // add lazy step to proof - d_proof.addLazyStep(lit, &d_factPg, false); + d_proof.addLazyStep(lit, &d_factPg); // second, assert it to the equality engine Node reason = NodeManager::currentNM()->mkAnd(exp); return assertFactInternal(atom, polarity, reason); @@ -116,7 +116,7 @@ bool ProofEqEngine::assertFact(Node lit, ps.d_args = args; d_factPg.addStep(lit, ps); // add lazy step to proof - d_proof.addLazyStep(lit, &d_factPg, false); + d_proof.addLazyStep(lit, &d_factPg); // second, assert it to the equality engine return assertFactInternal(atom, polarity, exp); } @@ -140,7 +140,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb) d_factPg.addStep(step.first, step.second); } // add lazy step to proof - d_proof.addLazyStep(lit, &d_factPg, false); + d_proof.addLazyStep(lit, &d_factPg); // second, assert it to the equality engine return assertFactInternal(atom, polarity, exp); } @@ -157,7 +157,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg) return false; } // note the proof generator is responsible for remembering the explanation - d_proof.addLazyStep(lit, pg, false); + d_proof.addLazyStep(lit, pg); // second, assert it to the equality engine return assertFactInternal(atom, polarity, exp); } |