diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-26 08:51:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-26 08:51:57 -0500 |
| commit | 6ad02b5e0599149e0bd1548855aec8ac890f5a87 (patch) | |
| tree | 5607fd85c45102426314241f193bec9bc2308040 /src/theory/ext_theory.cpp | |
| parent | 160a3f55bf4dbfdbc1385ce4898c62b1fd3a8c78 (diff) | |
Use original quantified formula for single invocation reconstruction (#5129)
This fixes an issue with single invocation solution reconstruction where the preprocessed quantified formula contains internal skolems, thus prohibiting reconstruction. The solution is to use the original quantified formula when doing solution reconstruction. This adds a regression demonstrating the issue.
Diffstat (limited to 'src/theory/ext_theory.cpp')
0 files changed, 0 insertions, 0 deletions