diff options
Diffstat (limited to 'src/smt/proof_post_processor.cpp')
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index adc15ca2c..04a36c1c0 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -42,7 +42,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env, : d_env(env), d_pnm(env.getProofNodeManager()), d_pppg(pppg), - d_wfpm(env.getProofNodeManager()), + d_wfpm(env), d_updateScopedAssumptions(updateScopedAssumptions) { d_true = NodeManager::currentNM()->mkConst(true); @@ -654,7 +654,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // apply transitivity if necessary Node eq = addProofForTrans(tchildren, cdp); - cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {}); + cdp->addStep(eq[1], PfRule::EQ_RESOLVE, {children[0], eq}, {}); return args[0]; } else if (id == PfRule::MACRO_RESOLUTION |