NEWS

--- a/NEWS	Tue Nov 03 14:51:55 2009 +0100
+++ b/NEWS	Tue Nov 03 17:54:24 2009 +0100
@@ -55,6 +55,10 @@
 this method is proof-producing. Certificates are provided to
 avoid calling the external solvers solely for re-checking proofs.
 
+* New commands to load and prove verification conditions
+generated by the Boogie program verifier or derived systems
+(e.g. the Verifying C Compiler (VCC) or Spec#).
+
 * New counterexample generator tool "nitpick" based on the Kodkod
 relational model finder.