diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-29 09:57:35 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-29 09:57:35 -0500 |
| commit | 69e1472971f4aae9771630f911565a6f4548894b (patch) | |
| tree | eb631081df70474e3a93ff5ffb5d9c9b97aed45d /src/smt/proof_manager.h | |
| parent | 1c9290c99daa69b549d49dc762cadd8307211bc8 (diff) | |
(proof-new) Fixes for preprocess proof generator and proofs in assertion pipeline (#5136)
This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline.
Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.
Diffstat (limited to 'src/smt/proof_manager.h')
| -rw-r--r-- | src/smt/proof_manager.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index bda741a05..118b82bec 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -41,7 +41,7 @@ class Assertions; class PfManager { public: - PfManager(SmtEngine* smte); + PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); /** * Print the proof on the output channel of the current options in scope. |