Updated version number to 1.9.9

Dafny version 1.9.9 includes the following changes over version 1.9.8:

Language

* Allow TLA+ style conjunctions and disjunctions.

* Allow the first datatype constructor to be preceded by a `|`.

* Destructor names can now be shared among datatype constructors.

* Added two-state functions and two-state predicates.

* Two-state lemmas no longer support `reads` clauses.  Instead,
  use the new `unchanged` predicate.

* Added `unchanged` predicate, which takes a frame argument and says
  those things are the same in the pre- and post-states.

* `fresh` applied to a collection now says that all elements of the
  collection are `fresh`.  This is a change in semantics from before.

* `allocated` predicate (re-)introduced.  It says that its argument
  is available in the state.

* Inside an `old`, disallow `unchanged`, `fresh`, two-state functions,
  two-state lemmas, and nested `old`.

* Added `const` declarations.

* Added conversions between `char` an integral types.

* Function results can now be named, for use in the function's
  postcondition.

* Added operations that rotate bits in bitvectors.

* `map` and `imap` now have `.Keys`, `.Values`, and `.Items` members.

* Language support for revealing `{:opaque}` functions.  Use
  `reveal F()` instead of the previous `reveal_F()`.

* Support for tuples in `match` constructs.

* Expand the repertoire of constructs where co-recursive function calls are recognized.

* Proper support for type parameters in inductive and co-inductive predicates.

* Allow `reads` clauses on inductive and co-inductive predicates.

* Disallow parameters marked with `ghost` in signatures that are already ghost.

Modules

* Class members can be individually exported.

* Datatypes can now be exported as provided or revealed.

* All datatypes can be revealed by `reveal *`.

* Opened imports are not exported.

* `exclusively refines` is no longer supported.

* Module facades may now only be refined by explicit refinements.
  The previous structural checks are no longer supported.

Verification

* Improved string support

* More quantifier rewriting to help avoid matching loops, in particular
  address quantifiers like `forall i :: 1 <= i < a.Length ==> a[i-1] <= a[i]`

Pipeline

* Speed-ups in resolution and translation (and added `/optimizeResolution` flag).

* Set appropriate exit value for Dafny errors.

* Use .NET Framework 4.5.

* Use Z3 version 4.4.2 (private build Oct 2016).

IDEs

* Syntax highlight bitvectors in Visual Studio.

* Show some Boogie resolution errors in lieu of many a
  "Verification process error" in Visual Studio.

* Improved caching.

Advanced settings

* Improvement in manual fuel settings.

* `/allocated` option, which encodes allocatedness in alternate ways.

* `/printIncludes` option.

* `/disableScopes` option.

* Handle `:warnShadowing` attribute on methods and lemmas.

* As an optimization, Boogie implementations with no proof obligations
  are no longer emitted.

* Don't verify modules that came from an include.

Miscellaneous

* Bug fixes in subset types.

* Various bug fixes, including many Issues reported on github.

Author: Rustan Leino

Source/Dafny/DafnyOptions.cs

@@ -28,7 +28,7 @@ public override string VersionNumber {
     }
     public override string VersionSuffix {
       get {
-        return " version " + VersionNumber + ", Copyright (c) 2003-2016, Microsoft.";
+        return " version " + VersionNumber + ", Copyright (c) 2003-2017, Microsoft.";
       }
     }
 

Source/version.cs

@@ -1,4 +1,4 @@
 using System.Reflection;
-// Version 1.9.8, year 2013+3 month 08 day 29
-[assembly: AssemblyVersion("1.9.8.30829")]
-[assembly: AssemblyFileVersion("1.9.8.30829")]
+// Version 1.9.9, year 2013+4 month 04 day 14
+[assembly: AssemblyVersion("1.9.9.40414")]
+[assembly: AssemblyFileVersion("1.9.9.40414")]