diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-21 14:07:08 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-21 21:07:08 +0000 |
| commit | f71d55abdbe6a51613a1ff33f24c708f66bf784e (patch) | |
| tree | 79b42e80172349a17dbbaf5d0f512947a3f9d71e /src | |
| parent | f3bf9af12eb6af487e61c585fa9639f1d1485220 (diff) | |
Also fix case of negated ite (#7454)
This PR follows #7452 and fixes the proofs generated for backward propagation of negated ite terms.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/booleans/proof_circuit_propagator.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index fa48f7638..71fb2a56f 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -402,7 +402,8 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c) true); } return mkResolution( - mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}), + mkProof(c == 0 ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2, + {assume(d_parent.notNode())}), d_parent[c + 1], false); } |