--- a/NEWS Tue Oct 20 08:10:47 2009 +0200
+++ b/NEWS Tue Oct 20 10:11:30 2009 +0200
@@ -46,7 +46,9 @@
arithmetic, and fixed-size bitvectors; there is also basic
support for higher-order features (esp. lambda abstractions).
It is an incomplete decision procedure based on external SMT
-solvers using the oracle mechanism.
+solvers using the oracle mechanism; for the SMT solver Z3,
+this method is proof-producing. Certificates are provided to
+avoid calling the external solvers solely for re-checking proofs.
* Reorganization of number theory:
* former session NumberTheory now named Old_Number_Theory