diff options
| author | guykatzz <katz911@gmail.com> | 2017-05-30 09:25:54 -0700 |
|---|---|---|
| committer | guykatzz <katz911@gmail.com> | 2017-05-30 09:25:54 -0700 |
| commit | 61623d7bfb05143e52013db3610b63d632e61d92 (patch) | |
| tree | 6adbf499b4c342f99d3f05e8bcc3b73dbd103d54 /src/options/smt_options | |
| parent | 84df84769e6762562c599432ea681f9fa0c7e0ff (diff) | |
print only labeled assertions as part of the unsat core
added the option dump-unsat-cores-full for printing the entire core, as before
Diffstat (limited to 'src/options/smt_options')
| -rw-r--r-- | src/options/smt_options | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/src/options/smt_options b/src/options/smt_options index 394e2382a..5f50ed202 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -47,6 +47,8 @@ option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produc after UNSAT/VALID, produce and check an unsat core (expensive) option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :notify notifyBeforeSearch output unsat cores after every UNSAT/VALID response +option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch + dump the full unsat core, including unlabeled assertions option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch support the get-assignment command @@ -115,35 +117,35 @@ expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :de expert-option decisionStep decision-step --decision-step unsigned :default 1 amount of getNext decision calls in the decision engine - + expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1 amount of resources spent for each bitblast step - + expert-option parseStep parse-step --parse-step unsigned :default 1 amount of resources spent for each command/expression parsing - + expert-option lemmaStep lemma-step --lemma-step unsigned :default 1 amount of resources spent when adding lemmas - + expert-option restartStep restart-step --restart-step unsigned :default 1 amount of resources spent for each theory restart - + expert-option cnfStep cnf-step --cnf-step unsigned :default 1 amount of resources spent for each call to cnf conversion - + expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1 amount of resources spent for each preprocessing step in SmtEngine - + expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1 amount of resources spent for quantifier instantiations - + expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1 amount of resources spent for each sat conflict (main sat solver) - + expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1 amount of resources spent for each sat conflict (bitvectors) - - + + expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 |