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 bb0cf1a00..81891acf7 100644 --- a/src/smt/options +++ b/src/smt/options @@ -32,6 +32,8 @@ option doStaticLearning static-learning /--no-static-learning bool :default true common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands +option checkModels check-models --check-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h" + after SAT/INVALID, double-check that the generated model satisfies all user assertions common-option produceAssignments produce-assignments --produce-assignments bool support the get-assignment command option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h" |