diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-17 17:40:34 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-17 17:40:40 -0500 |
| commit | 12a1b56a7a6573ae5af47e9d9d6e757e70a6b7a1 (patch) | |
| tree | c998399e536c044b2b1c43a94790b3fc02352ea8 /src/smt | |
| parent | 3ad29c402d240432032b9ddf18d9133f438e1236 (diff) | |
Add support for --dump-models option, in preparation for casc.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/options b/src/smt/options index 2680f4105..e5f9c2eaf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -24,6 +24,8 @@ common-option produceModels produce-models -m --produce-models bool :default fal support the get-value and get-model commands option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions +option dumpModels --dump-models bool :default false + output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation # this is just a placeholder for later; it doesn't show up in command-line options listings |