From c130a81b3578898dcb5cacaf746e4dd923e2c5d6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Aug 2019 13:23:07 -0500 Subject: Call separate SMT engine for single invocation sygus (#3151) --- src/options/quantifiers_options.toml | 18 ------------------ 1 file changed, 18 deletions(-) (limited to 'src/options') 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 @@ -940,24 +940,6 @@ header = "options/quantifiers_options.h" read_only = true 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" -- cgit v1.2.3