summaryrefslogtreecommitdiff
path: root/NEWS
diff options
context:
space:
mode:
Diffstat (limited to 'NEWS')
-rw-r--r--NEWS10
1 files changed, 9 insertions, 1 deletions
diff --git a/NEWS b/NEWS
index 8c93b1478..17a934729 100644
--- a/NEWS
+++ b/NEWS
@@ -3,7 +3,15 @@ This file contains a summary of important user-visible changes.
Changes since 1.1
=================
-* nothing notable yet
+* Real arithmetic now has three simplex solvers for exact precision linear
+ arithmetic: the classical dual solver and two new solvers based on
+ techniques for minimizing the sum of infeasibilities. GLPK can now be used
+ as a heuristic backup to the exact precision solvers. GLPK must be enabled
+ at configure time. See --help for more information on enabling these solvers.
+* added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
+* support for theory "alternates": new ability to prototype new decision
+ procedures that are selectable at runtime
+* various bugfixes
Changes since 1.0
=================
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback