diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-20 00:05:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-20 00:05:58 -0500 |
commit | 927066eaecfc2c6f00aa1aca695b68e70164aae3 (patch) | |
tree | 7456a1ec973f80aa806b66a8a2c6b6a8dfc3b4ba /src/options/smt_options.toml | |
parent | 7b4084440bd9dde894ff46c2ba0197fed41d91d1 (diff) |
Use debug-check-model to enable internal debugging in check-model (#4480)
Notice this also updates our regression script to use --debug-check-model, preserving previous behavior.
Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474.
Diffstat (limited to 'src/options/smt_options.toml')
-rw-r--r-- | src/options/smt_options.toml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 6ac5b0289..08e6f317c 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -80,10 +80,17 @@ header = "options/smt_options.h" long = "check-models" type = "bool" notifies = ["notifyBeforeSearch"] - read_only = true help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions" [[option]] + name = "debugCheckModels" + category = "regular" + long = "debug-check-models" + type = "bool" + notifies = ["notifyBeforeSearch"] + help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions" + +[[option]] name = "dumpModels" category = "regular" long = "dump-models" |