summaryrefslogtreecommitdiff
path: root/NEWS
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-12-04 16:04:14 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-12-04 17:13:47 -0500
commit863dd51bd8b5d72d41006a02950de28fc1666f21 (patch)
tree064a73d8a5bf75455010e7cacae126fd057c2c91 /NEWS
parent5e52f04e3deca668df1637ee9a11ecf0deb3bf27 (diff)
Don't put define-funs in model output; bug 411 testcase no longer relevant.
Diffstat (limited to 'NEWS')
-rw-r--r--NEWS2
1 files changed, 2 insertions, 0 deletions
diff --git a/NEWS b/NEWS
index 02779ed24..1ff3392ce 100644
--- a/NEWS
+++ b/NEWS
@@ -20,6 +20,8 @@ Changes since 1.2
zero means no error---but the result could be sat, unsat, or unknown---and
nonzero means error.
* bv2nat/int2bv functionality
+* User-defined symbols (define-funs) are no longer reported in the output
+ of get-model commands.
Changes since 1.1
=================
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback