diff options
Diffstat (limited to 'src/smt/dump.cpp')
| -rw-r--r-- | src/smt/dump.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index b1222a51e..ce146da0e 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -59,6 +59,8 @@ void DumpC::setDumpFromString(const std::string& optarg) { } else if(!strcmp(p, "boolean-terms")) { } else if(!strcmp(p, "constrain-subtypes")) { } else if(!strcmp(p, "substitution")) { + } else if(!strcmp(p, "bv-to-bool")) { + } else if(!strcmp(p, "bool-to-bv")) { } else if(!strcmp(p, "strings-pp")) { } else if(!strcmp(p, "skolem-quant")) { } else if(!strcmp(p, "simplify")) { @@ -163,9 +165,9 @@ assertions\n\ + Output the assertions after preprocessing and before clausification.\n\ Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ - simplify static-learning ite-removal repeat-simplify\n\ - rewrite-apply-to-const theory-preprocessing.\n\ + boolean-terms constrain-subtypes substitution bv-to-bool bool-to-bv\n\ + strings-pp skolem-quant simplify static-learning ite-removal\n\ + repeat-simplify rewrite-apply-to-const theory-preprocessing.\n\ PASS can also be the special value \"everything\", in which case the\n\ assertions are printed before any preprocessing (with\n\ \"assertions:pre-everything\") or after all preprocessing completes\n\ |