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/options/arith_options.toml | |
| 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/options/arith_options.toml')
| -rw-r--r-- | src/options/arith_options.toml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index da3a8dc88..fad1b3dcd 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -460,7 +460,6 @@ header = "options/arith_options.h" long = "nl-ext-tplanes" type = "bool" default = "false" - read_only = true help = "use non-terminating tangent plane strategy for non-linear incremental linearization solver" [[option]] |