Changing default language (#4561)

Useful to avoid issues when a language is not set and it cannot be easily inferred (for example via the API). Since the language that covers most operators in CVC4 is the SMT one we use that as default now.

3 files changed, 9 insertions, 6 deletions

diff --git a/NEWS b/NEWS
index 92cd3ee80..a7d6d3f40 100644
--- a/NEWS
+++ b/NEWS
@@ -9,6 +9,9 @@ Changes:
   `Result::Entailment` along with corresponding changes to the enum values.
 * Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
   instead of `edu.nyu.acsys.CVC4`.
+* The default output language is changed from CVC to SMT-LIB 2.6. The
+  default output language is used when the problem language cannot be
+  easily inferred (for example when CVC4 is used from the API).
 * Printing of BV constants: previously CVC4 would print BV constant
   values as indexed symbols by default and in binary notation with the
   option --bv-print-consts-in-binary. To be SMT-LIB compliant the
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index f8d62a8be..332af6e48 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -122,9 +122,10 @@ Printer* Printer::getPrinter(OutputLanguage lang)
       lang = language::toOutputLanguage(options::inputLanguage());
      }
    }
-   if(lang == language::output::LANG_AUTO) {
-      lang = language::output::LANG_CVC4; // default
-    }
+   if (lang == language::output::LANG_AUTO)
+   {
+     lang = language::output::LANG_SMTLIB_V2_6;  // default
+   }
   }
   if(d_printers[lang] == NULL) {
     d_printers[lang] = makePrinter(lang);
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 43554088f..3dcf18f78 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -416,9 +416,8 @@ void SolverBlack::testMkBitVector()
   TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
                    d_solver->mkBitVector("a", 16));
   TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(),
-                   "0bin01010101");
-  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(),
-                   "0bin00001111");
+                   "#b01010101");
+  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), "#b00001111");
   TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "-1", 10),
                    d_solver->mkBitVector(8, "FF", 16));
 }