diff options
Diffstat (limited to 'src/smt/options')
| -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 05a138f60..69b5102de 100644 --- a/src/smt/options +++ b/src/smt/options @@ -22,6 +22,8 @@ option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands +option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after UNSAT/VALID, machine-check the generated proof 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 |