From 7aa98fa461932db12c05820e685772d2aa983993 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 5 Jun 2020 11:10:34 -0300
Subject: [PATCH] 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.
---
 NEWS                         | 3 +++
 src/printer/printer.cpp      | 7 ++++---
 test/unit/api/solver_black.h | 5 ++---
 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));
 }
-- 
2.30.2