diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-14 13:23:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-14 13:23:07 -0500 |
| commit | c130a81b3578898dcb5cacaf746e4dd923e2c5d6 (patch) | |
| tree | 167e9bf516882cfb6c08f88b9110ca241a973f6a /src/options | |
| parent | 94af13b18b10d6092981848fbae1b9c35b27b31d (diff) | |
Call separate SMT engine for single invocation sygus (#3151)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options.toml | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 717ee9dae..00059bba6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -941,24 +941,6 @@ header = "options/quantifiers_options.h" help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" [[option]] - name = "cegqiSolMinCore" - category = "regular" - long = "cegqi-si-sol-min-core" - type = "bool" - default = "false" - read_only = true - help = "minimize solutions for single invocation conjectures based on unsat core" - -[[option]] - name = "cegqiSolMinInst" - category = "regular" - long = "cegqi-si-sol-min-inst" - type = "bool" - default = "true" - read_only = true - help = "minimize individual instantiations for single invocation conjectures based on unsat core" - -[[option]] name = "cegqiSingleInvAbort" category = "regular" long = "cegqi-si-abort" |