diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-18 19:37:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-18 19:37:11 -0500 |
commit | 547bd91e189b28da9950e12037d1e88079157479 (patch) | |
tree | 7f225e6df081071028c9e6102c902a6224179edf /src/options/smt_options.toml | |
parent | 10707e3ec6f2cab793919f2d1a159e13cdd032a9 (diff) |
Non-implied mode for model cores (#2653)
Diffstat (limited to 'src/options/smt_options.toml')
-rw-r--r-- | src/options/smt_options.toml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 8af1000ba..e0041774a 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -40,7 +40,7 @@ header = "options/smt_options.h" type = "SimplificationMode" default = "SIMPLIFICATION_MODE_BATCH" handler = "stringToSimplificationMode" - includes = ["options/simplification_mode.h"] + includes = ["options/smt_modes.h"] help = "choose simplification mode, see --simplification=help" [[alias]] @@ -99,13 +99,14 @@ header = "options/smt_options.h" help = "output models after every SAT/INVALID/UNKNOWN response" [[option]] - name = "produceModelCores" + name = "modelCoresMode" category = "regular" - long = "produce-model-cores" - type = "bool" - default = "false" - read_only = true - help = "when printing models, compute a minimal core of relevant definitions" + long = "model-cores=MODE" + type = "ModelCoresMode" + default = "MODEL_CORES_NONE" + handler = "stringToModelCoresMode" + includes = ["options/smt_modes.h"] + help = "mode for producing model cores" [[option]] name = "proof" |