diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-12 18:24:54 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-16 22:28:26 -0500 |
| commit | 5186ca79710fe935d1f7ed27c4a34e913ab547e8 (patch) | |
| tree | 4f5ce4957063085f607492a6474b0d244e4b2da4 /src/smt/options | |
| parent | 4d9caf9782c59823fb95519b9b518b7d7f89738a (diff) | |
First attempt at incorporating LFSC proof checker into CVC4.
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 |