Minor cleanup of proof messages (#7494)

[cvc5.git] / NEWS

diff --git a/NEWS b/NEWS
index 74ee8616548a6850a5009bbcfd9e0473014b588d..c9716b33f9e67e6e6042f3d05df24223549733de 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -23,6 +23,7 @@ New Features:
   * Support for `str.indexof_re(s, r, n)`, which returns the index of the first
     occurrence of a regular expression `r` in a string `s` after index `n` or
     -1 if `r` does not match a substring after `n`.
+* A new option to compute minimal unsat cores (`--minimal-unsat-cores`).
 
 Improvements:
 * New API: Added functions to retrieve the heap/nil term when using separation
@@ -30,7 +31,8 @@ Improvements:
 
 Changes:
 * SyGuS: Removed support for SyGuS-IF 1.0.
-* Removed Java and Python bindings for the legacy API
+* Removed support for the (non-standard) `define` command.
+* Removed Java and Python bindings for the legacy API.
 * Interactive shell: the GPL-licensed Readline library has been replaced the
   BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
   of Readline. Without selecting optional GPL components, Editline-enabled CVC4