Bump Boogie to v2.16.8

Source/DafnyCore/DafnyCore.csproj

@@ -32,7 +32,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.5" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.8" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/DafnyOptions.cs

@@ -239,6 +239,7 @@ public DafnyOptions(TextReader inputReader, TextWriter outputWriter, TextWriter
       ErrorWriter = errorWriter;
       ErrorTrace = 0;
       Prune = true;
+      TypeEncodingMethod = Bpl.CoreOptions.TypeEncoding.Predicates;
       NormalizeNames = true;
       EmitDebugInformation = false;
       Backend = new CsharpBackend(this);

customBoogie.patch

@@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644
        <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
        <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
        <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
--      <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.5" />
+-      <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.8" />
 +      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
        <PackageReference Include="Tomlyn" Version="0.16.2" />
    </ItemGroup>

docs/DafnyRef/Options.txt

@@ -590,8 +590,8 @@ Usage: dafny [ option ... ] [ filename ... ]
                 do not verify layers <n> and below
   /trustLayersDownto:<n>
                 do not verify layers <n> and above
-  /trustInductiveSequentialization
-                do not perform inductive sequentialization checks
+  /trustSequentialization
+                do not perform sequentialization checks
   /civlDesugaredFile:<file>
                 print plain Boogie program to <file>
 
@@ -653,18 +653,17 @@ Usage: dafny [ option ... ] [ filename ... ]
                 invocation during smoke test, defaults to 10.
   /causalImplies
                 Translate Boogie's A ==> B into prover's A ==> A && B.
-  /typeEncoding:<m>
+  /typeEncoding:<t>
                 Encoding of types when generating VC of a polymorphic program:
-                   p = predicates (default)
+                   m = monomorphic (default)
+                   p = predicates
                    a = arguments
                 Boogie automatically detects monomorphic programs and enables
                 monomorphic VC generation, thereby overriding the above option.
-  /monomorphize
-                Try to monomorphize program. An error is reported if
-                monomorphization is not possible. This feature is experimental!
-  /useArrayTheory
-                Use the SMT theory of arrays (as opposed to axioms). Supported
-                only for monomorphic programs.
+                If the latter two options are used, then arrays are handled via axioms.
+  /useArrayAxioms
+                If monomorphic type encoding is used, arrays are handled by default with
+                the SMT theory of arrays. This option allows the use of axioms instead.
   /reflectAdd   In the VC, generate an auxiliary symbol, elsewhere defined
                 to be +, instead of +.
   /prune
@@ -678,10 +677,8 @@ Usage: dafny [ option ... ] [ filename ... ]
   /relaxFocus   Process foci in a bottom-up fashion. This way only generates
                 a linear number of splits. The default way (top-down) is more
                 aggressive and it may create an exponential number of splits.
-
   /randomSeed:<s>
                 Supply the random seed for /randomizeVcIterations option.
-
   /randomizeVcIterations:<n>
                 Turn on randomization of the input that Boogie passes to the
                 SMT solver and turn on randomization in the SMT solver itself.