From 111a197b4d9179a92b0509aded6463d47e036cc0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Oct 2020 14:30:02 -0500 Subject: 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. --- src/options/arith_options.toml | 1 - 1 file changed, 1 deletion(-) (limited to 'src/options/arith_options.toml') 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]] -- cgit v1.2.3