diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-25 21:00:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-25 19:00:13 -0800 |
| commit | d0c352ec04846353d630073e78e5b2fea92133c2 (patch) | |
| tree | 41255824f4f72f0eccbc7dbb2402cb46b5b9e54a /test/unit/theory/theory_white.h | |
| parent | 084518db641e0648164bbe4461cd98b10e937dc0 (diff) | |
Fix missed case of theory preprocessing (#5531)
This fixes a rare case of theory preprocessing where rewriting a quantified formula would introduce a term that would not be preprocessed. This led to solution unsoundness on a branch where the relationship between expand definitions and preprocessing is modified.
This is required for updating to the new policy for expand definitions.
Diffstat (limited to 'test/unit/theory/theory_white.h')
0 files changed, 0 insertions, 0 deletions