diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-17 21:38:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-17 21:38:42 -0500 |
| commit | 89c5d4ac65f45f24a7dc0ab76bb2bdb447bdfcda (patch) | |
| tree | cd827a431bbd9122b683dee079869f253c0299ac /src/theory/strings/solver_state.h | |
| parent | cb438c1aca9e205359313f2e661fef910e1132b6 (diff) | |
(proof-new) Updates to proof node updater algorithm (#5088)
This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating.
This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.
Diffstat (limited to 'src/theory/strings/solver_state.h')
0 files changed, 0 insertions, 0 deletions