From 7aa98fa461932db12c05820e685772d2aa983993 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 5 Jun 2020 11:10:34 -0300 Subject: 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 +++ 1 file changed, 3 insertions(+) (limited to 'NEWS') 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 -- cgit v1.2.3