From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 3 Apr 2013 16:53:15 +0000 (-0400)
Subject: updated NEWS to include inequality solver
X-Git-Tag: cvc5-1.0.0~7334
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c9c41118eb3af8c882019a6e978e838ac793002d;p=cvc5.git

updated NEWS to include inequality solver
---

diff --git a/NEWS b/NEWS
index e792564ba..844610486 100644
--- a/NEWS
+++ b/NEWS
@@ -3,6 +3,8 @@ This file contains a summary of important user-visible changes.
 Changes since 1.0
 =================
 
+* bit-vector solver now has a specialized decision procedure for unsigned bit-
+  vector inequalities
 * tuple and record support in the compatibility library
 * user patterns are now supported in the SMT-LIBv1.2 parser
 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)