diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-01 17:14:06 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-01 17:14:06 -0700 |
| commit | 5ae076e726a013039c8392277437902600359b17 (patch) | |
| tree | 3c840960cdf0199d9f7fe78fafaf2f8e79365c39 /src/proof/lazy_proof.cpp | |
| parent | b1582722951f6925d3422ec21906d24f5c8cdfc0 (diff) | |
| parent | 351fe43811e35f04ced22ca459fa31f7dd94937f (diff) | |
Merge branch 'master' into macos11macos11
Diffstat (limited to 'src/proof/lazy_proof.cpp')
| -rw-r--r-- | src/proof/lazy_proof.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp index b16a8d758..eab452d49 100644 --- a/src/proof/lazy_proof.cpp +++ b/src/proof/lazy_proof.cpp @@ -100,7 +100,14 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) if (isSym) { - d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + if (pgc->getRule() == PfRule::SYMM) + { + d_manager->updateNode(cur, pgc->getChildren()[0].get()); + } + else + { + d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + } } else { |