diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-30 13:59:52 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-08 16:52:20 -0400 |
| commit | 843cfdae175f8ef6fc3c7a3e3a5fa4e7f37863e1 (patch) | |
| tree | 17595d0a8b78f3e4d050b6abec7547118edd86c0 /NEWS | |
| parent | a2c0fd92782ce942a6f25f2561a4918fb2c5b020 (diff) | |
update versioningsmteval2013
Diffstat (limited to 'NEWS')
| -rw-r--r-- | NEWS | 10 |
1 files changed, 9 insertions, 1 deletions
@@ -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 ================= |