diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-05 14:30:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-05 14:30:02 -0500 |
| commit | 111a197b4d9179a92b0509aded6463d47e036cc0 (patch) | |
| tree | 7107acd35c38640b65d539935f79c8db4be7b197 /src/util/integer_gmp_imp.h | |
| parent | 13cf41801f8f2bac538cb45d53ae7427916041a7 (diff) | |
Make sygus more robust to unknown responses in solution verification (#5199)
This makes it so that an "unknown" response in a CEGIS verification step causes the sygus solver to exclude the current solution and mark incomplete. Previously, the sygus solver was non-terminating in such cases, trying the same solution continously.
This also removes the option "sygusVerifySubcall", as this option should always be used. It also makes --nl-ext-tplanes enabled by default when sygus is enabled.
Diffstat (limited to 'src/util/integer_gmp_imp.h')
0 files changed, 0 insertions, 0 deletions