Change option names --default-dag-thresh and --default-expr-depth (#4309)

5 files changed, 8 insertions, 8 deletions

diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index 546d9ee9c..111f71852 100644
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -38,7 +38,7 @@ int main()
   Solver slv;
   slv.setOption("produce-models", "true");  // Produce Models
   slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's
-  slv.setOption("default-dag-thresh", "0"); // Disable dagifying the output
+  slv.setOption("dag-thresh", "0"); // Disable dagifying the output
   slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
   slv.setLogic(string("QF_UFLIRA"));
 
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 2e972a543..a3d25d7f0 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -45,7 +45,7 @@ int main() {
   SmtEngine smt(&em);
   smt.setOption("produce-models", true); // Produce Models
   smt.setOption("output-language", "cvc4"); // Set the output-language to CVC's
-  smt.setOption("default-dag-thresh", 0); //Disable dagifying the output
+  smt.setOption("dag-thresh", 0); //Disable dagifying the output
   smt.setLogic(string("QF_UFLIRA"));
 
   // Sorts
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 53b1fa92d..1299e2928 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -42,7 +42,7 @@ public class Combination {
     smt.setOption("tlimit", new SExpr(100));
     smt.setOption("produce-models", new SExpr(true)); // Produce Models
     smt.setOption("output-language", new SExpr("cvc4")); // output-language
-    smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output
+    smt.setOption("dag-thresh", new SExpr(0)); //Disable dagifying the output
     smt.setLogic("QF_UFLIRA");
 
     // Sorts
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index 7a8055bdf..bae2b6ef9 100755
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -26,7 +26,7 @@ if __name__ == "__main__":
     slv = pycvc4.Solver()
     slv.setOption("produce-models", "true")  # Produce Models
     slv.setOption("output-language", "cvc4") # Set the output-language to CVC's
-    slv.setOption("default-dag-thresh", "0") # Disable dagifying the output
+    slv.setOption("dag-thresh", "0") # Disable dagifying the output
     slv.setOption("output-language", "smt2") # use smt-lib v2 as output language
     slv.setLogic("QF_UFLIRA")
 
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 741706070..4bdecf7ef 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -47,7 +47,7 @@ const struct option longopts[] = {
   { "output-language", required_argument, NULL, OUTPUT_LANG },
   { "expand-definitions", no_argument, NULL, EXPAND_DEFINITIONS },
   { "combine-assertions", no_argument, NULL, COMBINE_ASSERTIONS },
-  { "default-dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
+  { "dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
   { "lang", required_argument, NULL, INPUT_LANG },
   { "language", required_argument, NULL, INPUT_LANG },
   { "out", required_argument, NULL, OUTPUT_FILE },
@@ -60,7 +60,7 @@ static void showHelp() {
        << "  --output-language | -O  set output language (default smt2)" << endl
        << "  --input-language | -L   set input language (default auto)" << endl
        << "  --out | -o              set output file (- for stdout)" << endl
-       << "  --default-dag-thresh=N  set DAG threshold" << endl
+       << "  --dag-thresh=N  set DAG threshold" << endl
        << "  --expand-definitions    expand define-funs" << endl
        << "  --combine-assertions    combine all assertions into one" << endl
        << "  --help | -h             this help" << endl
@@ -237,14 +237,14 @@ int main(int argc, char* argv[]) {
         break;
       case DEFAULT_DAG_THRESH: {
           if(!isdigit(*optarg)) {
-            cerr << "error: --default-dag-thresh requires non-negative argument: `"
+            cerr << "error: --dag-thresh requires non-negative argument: `"
                  << optarg << "' invalid." << endl;
             exit(1);
           }
           char* end;
           unsigned long ul = strtoul(optarg, &end, 10);
           if(errno != 0 || *end != '\0') {
-            cerr << "error: --default-dag-thresh argument malformed: `"
+            cerr << "error: --dag-thresh argument malformed: `"
                  << optarg << "'." << endl;
             exit(1);
           }