diff options
| -rw-r--r-- | NEWS | 3 | ||||
| -rw-r--r-- | src/printer/printer.cpp | 7 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 5 |
3 files changed, 9 insertions, 6 deletions
@@ -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)); } |