From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 25 Jun 2018 21:27:20 +0000 (-0700)
Subject: More updates to NEWS for 1.6.
X-Git-Tag: cvc5-1.0.0~4951
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ded58d5e3b4046c48578078fe8d3cfd19f70c14;p=cvc5.git

More updates to NEWS for 1.6.
---

diff --git a/NEWS b/NEWS
index a9ce4d68f..038b02026 100644
--- 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