diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-10 10:27:44 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-10 10:27:44 -0600 |
| commit | b6df05346a3bd8c1c68ef74635711ff3e6bd5791 (patch) | |
| tree | 19d7fc01ebe2435cc3bbdc9756e01e55bd143e3c /src/theory/term_registration_visitor.cpp | |
| parent | e9408ca21267616bb799ef5f7fda85a1fee9c07c (diff) | |
Fix open proof for factoring lemma (#5885)
We need to add to the current proof, regardless of whether we have used the factor skolem previously.
Fixes bugs found by @HanielB on SMT-LIB runs.
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
0 files changed, 0 insertions, 0 deletions