diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-29 13:27:44 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-29 13:27:44 -0600 |
| commit | ce1b2f2fb06150599c231bf0d59b52a07e74c3f5 (patch) | |
| tree | 53fee982175e433e70ca5abe60a81b763c42f81f /src/smt/witness_form.cpp | |
| parent | 145b99d771e182fba70402398702ed12e3303682 (diff) | |
(proof-new) Distinguish pre vs post rewrites in term conversion proof generator (#5833)
This is work towards resolving two kinds of failures on proof-new:
(1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things,
(2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected.
A followup PR will simplify and fix proofs for theory-preprocessing.
Diffstat (limited to 'src/smt/witness_form.cpp')
| -rw-r--r-- | src/smt/witness_form.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 9c2c035a8..cba3bd340 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -118,7 +118,8 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) true, "WitnessFormGenerator::convertToWitnessForm:witness_axiom"); d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); - d_tcpg.addRewriteStep(cur, curw, &d_wintroPf, PfRule::ASSUME, true); + d_tcpg.addRewriteStep( + cur, curw, &d_wintroPf, true, PfRule::ASSUME, true); } else { |