summaryrefslogtreecommitdiff
path: root/NEWS
diff options
context:
space:
mode:
Diffstat (limited to 'NEWS')
-rw-r--r--NEWS3
1 files changed, 3 insertions, 0 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback