summaryrefslogtreecommitdiff
path: root/NEWS
diff options
context:
space:
mode:
Diffstat (limited to 'NEWS')
-rw-r--r--NEWS3
1 files changed, 3 insertions, 0 deletions
diff --git a/NEWS b/NEWS
index bd54ae81a..bd7347a75 100644
--- a/NEWS
+++ b/NEWS
@@ -4,7 +4,10 @@ Changes since 1.2
=================
* SMT-LIB support for abs, to_real, to_int, is_int
+* Expr::substitute() now capable of substituting operators (e.g.,
+ function symbols under an APPLY_UF)
* Support in linear logics for /, div, and mod by constants.
+* Support for TPTP's TFF and TFA formats.
* We no longer permit model or proof generation if there's been an
intervening push/pop.
* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback