More updates to NEWS for 1.6.
authorAina Niemetz <aina.niemetz@gmail.com>
Mon, 25 Jun 2018 21:27:20 +0000 (14:27 -0700)
committerAina Niemetz <aina.niemetz@gmail.com>
Mon, 25 Jun 2018 21:27:20 +0000 (14:27 -0700)
NEWS

diff --git a/NEWS b/NEWS
index a9ce4d68f7d26f50d62cf465d32104b3efcf5b5b..038b02026129d372fc35eca853481a94001f374d 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -8,7 +8,8 @@ New Features:
 * Novel approach for solving quantified bit-vectors (BV).
 * Eager bit-blasting: Support for SAT solver CaDiCaL.
 * A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
-* Support for transcendental functions (sin, cos, exp).
+* Support for transcendental functions (sin, cos, exp). In SMT2 input, this
+  can be enabled by adding T to the logic (e.g., QF_NRAT).
 * Support for new operators in strings, including string inequality (str.<=)
   and string code (str.code).
 * Support for automated rewrite rule generation from sygus (*.sy) inputs using
@@ -16,7 +17,6 @@ New Features:
 
 Improvements:
 * Incremental unsat core support.
-* Strings rewriter.
 * Further development of rewrite rules for the theory of strings and regular
   expressions.
 * Many optimizations for syntax-guided synthesis, including improved symmetry