Bump Boogie to v2.16.8 (#4044)

No major user-visible changes, but it should make the pool of solver
threads behave better, and may bring us a step closer to being able to
use Boogie's `/monomorphize` option with Dafny.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Remy Willems <rwillems@amazon.com>

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.