diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-12 10:56:25 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-12 10:56:25 -0600 |
| commit | 3b79066c39054efb95fdb71c3727482764e8a064 (patch) | |
| tree | 04191ee73293b81a6033231f8d58ffa875780651 /contrib | |
| parent | 4f367612a386d21315cee7d377176bc83a1402c5 (diff) | |
Fix redundant refinement lemma in sygus solver (#5399)
This ensures we do manual exclusion of candidate solutions that have counterexamples that are repeated, in particular in the case where the synthesis conjecture has no free variables.
This PR removes special casing for ground synthesis conjectures and fixes the exclusion during the refinement stage of sygus.
This is a prerequisite for updating arithmetic to not eliminate extended operators at expand definitions, which forces this feature to be exercised in a number of regressions.
Diffstat (limited to 'contrib')
0 files changed, 0 insertions, 0 deletions