NEWS

--- a/NEWS	Fri Nov 06 14:42:42 2009 +0100
+++ b/NEWS	Fri Nov 06 17:52:57 2009 +0100
@@ -54,6 +54,8 @@
 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.
+Due to a remote SMT service there is no need for installing SMT
+solvers locally.
 
 * New commands to load and prove verification conditions
 generated by the Boogie program verifier or derived systems