Add more NEWS (#2859)

diff --git a/NEWS b/NEWS
index f36460a275bf3b4ae0c9b693f9a0a5ccb6bf9782..7a7c9ba29876c283c5081444c4b18db358e527ed 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -4,9 +4,28 @@ Changes since 1.6
 =================
 
 New Features:
-* Strings: Support for `str.replaceall` operator.
+* Proofs:
+  * Support for bit-vector proofs with eager bitblasting (older versions only
+    supported proofs with lazy bitblasting).
+* Strings:
+  * Support for `str.replaceall` operator.
+  * New option `--re-elim` to reduce regular expressions to extended string
+    operators, resulting in better performance on regular expression benchmarks
+    (enabled by default).
+* SyGuS:
+  * Support for abduction (`--sygus-abduct`). Given a formula, this option uses
+    CVC4's SyGuS solver to find a sufficient condition such that the
+    conjunction of the condition and the formula is unsatisfiable.
+  * Support for two new term enumerator strategies: variable agnostic
+    (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
+    By default, CVC4 tries to choose the best term enumerator strategy
+    automatically based on the input (`--sygus-active-gen=auto`).
 
 Improvements:
+* Strings:
+  * Significantly better performance on string benchmarks over the core theory
+    and those with extended string functions like substring, contains, and
+    replace.
 
 Changes:
 * API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
@@ -14,7 +33,7 @@ Changes:
 * Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
 * The CVC3 compatibility layer has been removed.
 * The build system now uses CMake instead of Autotools. Please refer to
-* [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
+  [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
   up-to-date instructions on how to build CVC4.
 
 Changes since 1.5