diff options
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 338f5544f..b3c1ffd4d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1221,6 +1221,14 @@ header = "options/quantifiers_options.h" default = "false" help = "enable efficient support for recursive functions in sygus grammars" +[[option]] + name = "sygusRecFunEvalLimit" + category = "regular" + long = "sygus-rec-fun-eval-limit=N" + type = "int" + default = "1000" + help = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)" + # Internal uses of sygus [[option]] @@ -1359,7 +1367,7 @@ header = "options/quantifiers_options.h" long = "sygus-expr-miner-check-timeout=N" type = "unsigned long" help = "timeout (in milliseconds) for satisfiability checks in expression miners" - + [[option]] name = "sygusRewSynthRec" category = "regular" @@ -1420,7 +1428,7 @@ header = "options/quantifiers_options.h" default = "false" help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" - + [[option]] name = "sygusExprMinerCheckUseExport" category = "expert" |