Macos13and updated boogie

.github/workflows/doc-tests.yml

@@ -36,12 +36,11 @@ jobs:
         submodules: recursive
         path: dafny
     - name: Load Z3
+      with:
+        path: dafny
       run: |
         sudo apt-get install -qq libarchive-tools
-        mkdir -p dafny/Binaries/z3/bin
-        wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
-        mv z3-* dafny/Binaries/z3/bin/
-        chmod +x dafny/Binaries/z3/bin/z3-*
+        make z3-ubuntu
     - name: Build Dafny
       run: dotnet build dafny/Source/Dafny.sln
     - name: Check generated error catalog

.github/workflows/release-downloads-nuget.yml

@@ -32,7 +32,7 @@ jobs:
       fail-fast: false
       matrix:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-22.04, ubuntu-20.04, macos-11, windows-2019 ]
+        os: [ ubuntu-22.04, ubuntu-20.04, macos-13, windows-2019 ]
 
     steps:
     - name: OS

.github/workflows/release-downloads.yml

@@ -25,7 +25,7 @@ jobs:
         - os:  'ubuntu-20.04'
           osn: 'ubuntu-20.04'
         - os:  'macos-13'
-          osn: 'x64-macos-11'
+          osn: 'x64-macos-13'
         - os:  'windows-2019'
           osn: 'windows-2019'
     # There is no hosted environment for Ubuntu 14.04 or for debian

.github/workflows/standard-libraries.yml

@@ -17,7 +17,7 @@ jobs:
   build:
     needs: check-deep-tests
     if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
-    runs-on: macos-11
+    runs-on: macos-13
 
     steps:
       - name: Checkout Dafny

.github/workflows/xunit-tests-reusable.yml

@@ -49,10 +49,10 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-20.04, windows-2019, macos-11]
+        os: [ubuntu-20.04, windows-2019, macos-13]
         iteration: ${{ fromJson(needs.populate-matrix-dimensions.outputs.iterations) }}
         include:
-          - os: macos-11
+          - os: macos-13
             suffix: osx
             chmod: true
           - os: windows-2019
@@ -63,7 +63,7 @@ jobs:
             chmod: true
     env:
       solutionPath: Source/Dafny.sln
-      z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
+      z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10
       Logging__LogLevel__Microsoft: Debug
     steps:
     - uses: actions/checkout@v4

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "Test/libraries"]
 	path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
 	url = https://github.com/dafny-lang/libraries.git
+[submodule "boogie"]
+	path = boogie
+	url = [email protected]:keyboardDrummer/boogie.git

Makefile

@@ -1,4 +1,5 @@
 DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))
+BIN=$(DIR)/Binaries/net8.0/
 
 default: exe
 
@@ -39,37 +40,37 @@ refman-release: exe
 	make -C "${DIR}"/docs/DafnyRef release
 
 z3-mac:
-	mkdir -p "${DIR}"/Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
-	unzip z3-4.12.1-x64-macos-11-bin.zip
-	rm z3-4.12.1-x64-macos-11-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
-	unzip z3-4.8.5-x64-macos-11-bin.zip
-	rm z3-4.8.5-x64-macos-11-bin.zip
-	mv z3-* "${DIR}"/Binaries/z3/bin/
-	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
+	mkdir -p "${BIN}"/z3/bin
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.1-x64-macos-13-bin.zip
+	unzip z3-4.12.1-x64-macos-13-bin.zip
+	rm z3-4.12.1-x64-macos-13-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.6-x64-macos-13-bin.zip
+	unzip z3-4.12.6-x64-macos-13-bin.zip
+	rm z3-4.12.6-x64-macos-13-bin.zip
+	mv z3-* "${BIN}"/z3/bin/
+	chmod +x "${BIN}"/z3/bin/z3-*
 
 z3-mac-arm:
-	mkdir -p "${DIR}"/Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip
-	unzip z3-4.12.1-arm64-macos-11-bin.zip
-	rm z3-4.12.1-arm64-macos-11-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
-	unzip z3-4.8.5-x64-macos-11-bin.zip
-	rm z3-4.8.5-x64-macos-11-bin.zip
-	mv z3-* "${DIR}"/Binaries/z3/bin/
-	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
+	mkdir -p "${BIN}"/z3/bin
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.1-arm64-macos-13-bin.zip
+	unzip z3-4.12.1-arm64-macos-13-bin.zip
+	rm z3-4.12.1-arm64-macos-13-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.6-x64-macos-13-bin.zip
+	unzip z3-4.12.6-x64-macos-13-bin.zip
+	rm z3-4.12.6-x64-macos-13-bin.zip
+	mv z3-* "${BIN}"/z3/bin/
+	chmod +x "${BIN}"/z3/bin/z3-*
 
 z3-ubuntu:
-	mkdir -p "${DIR}"/Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
+	mkdir -p "${BIN}"/z3/bin
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.1-x64-ubuntu-20.04-bin.zip
 	unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
 	rm z3-4.12.1-x64-ubuntu-20.04-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-ubuntu-20.04-bin.zip
-	unzip z3-4.8.5-x64-ubuntu-20.04-bin.zip
-	rm z3-4.8.5-x64-ubuntu-20.04-bin.zip
-	mv z3-* "${DIR}"/Binaries/z3/bin/
-	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.6-x64-ubuntu-20.04-bin.zip
+	unzip z3-4.12.6-x64-ubuntu-20.04-bin.zip
+	rm z3-4.12.6-x64-ubuntu-20.04-bin.zip
+	mv z3-* "${BIN}"/z3/bin/
+	chmod +x "${BIN}"/z3/bin/z3-*
 
 format:
 	dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs

Scripts/dafny

@@ -17,7 +17,7 @@ if [ "${MY_OS:0:5}" == "MINGW" ] || [ "${MY_OS:0:6}" == "CYGWIN" ]; then
 else
     DAFNY_EXE_NAME="Dafny.dll"
 fi
-DAFNY="$DAFNY_ROOT/Binaries/$DAFNY_EXE_NAME"
+DAFNY="$DAFNY_ROOT/Binaries/net8.0/$DAFNY_EXE_NAME"
 if [[ ! -e "$DAFNY" ]]; then
     echo "Error: $DAFNY_EXE_NAME not found at $DAFNY."
     exit 1

Source/AutoExtern.Test/AutoExtern.Test.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
     <IsPackable>false</IsPackable>

Source/AutoExtern.Test/Minimal/Library.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
   <PropertyGroup>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
   </PropertyGroup>

Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <NoWarn>CS3021; CS0162</NoWarn>
     <!-- <Nullable>enable</Nullable> -->

Source/AutoExtern.Test/Tutorial/Library/Library.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
   <PropertyGroup>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
   </PropertyGroup>

Source/AutoExtern/AutoExtern.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>

Source/Dafny.sln

@@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -138,5 +164,17 @@ Global
 		SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
+		{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
 	EndGlobalSection
 EndGlobal

Source/Dafny/Dafny.csproj

@@ -5,7 +5,7 @@
       <AssemblyName>Dafny</AssemblyName>
       <GenerateAssemblyInfo>true</GenerateAssemblyInfo>
       <DefineConstants>TRACE</DefineConstants>
-      <TargetFramework>net6.0</TargetFramework>
+      <TargetFramework>net8.0</TargetFramework>
       <OutputPath>..\..\Binaries\</OutputPath>
       <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
 

Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
     <PropertyGroup>
-        <TargetFramework>net6.0</TargetFramework>
+        <TargetFramework>net8.0</TargetFramework>
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>enable</Nullable>
         <OutputPath>..\..\Binaries\</OutputPath>

Source/DafnyCore.Test/DafnyCore.Test.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
     <PropertyGroup>
-        <TargetFramework>net6.0</TargetFramework>
+        <TargetFramework>net8.0</TargetFramework>
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>enable</Nullable>
 

Source/DafnyCore/AST/AstVisitor.cs

@@ -115,7 +115,7 @@ public void VisitMember(MemberDecl member) {
 
       } else {
         Contract.Assert(false);
-        throw new cce.UnreachableException(); // unexpected member type
+        throw new Cce.UnreachableException(); // unexpected member type
       }
     }
 

Source/DafnyCore/AST/Attributes.cs

@@ -19,7 +19,7 @@ public class Attributes : TokenNode {
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Name != null);
-    Contract.Invariant(cce.NonNullElements(Args));
+    Contract.Invariant(Cce.NonNullElements(Args));
   }
 
   public static string AxiomAttributeName = "axiom";
@@ -36,7 +36,7 @@ void ObjectInvariant() {
   public readonly Attributes Prev;
   public Attributes(string name, [Captured] List<Expression> args, Attributes prev) {
     Contract.Requires(name != null);
-    Contract.Requires(cce.NonNullElements(args));
+    Contract.Requires(Cce.NonNullElements(args));
     Name = name;
     Args = args;
     Prev = prev;

Source/DafnyCore/AST/Cloner.cs

@@ -98,7 +98,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
       } else if (d is TupleTypeDecl) {
         // Tuple type declarations only exist in the system module. Therefore, they are never cloned.
         Contract.Assert(false);
-        throw new cce.UnreachableException();
+        throw new Cce.UnreachableException();
       } else if (d is IndDatatypeDecl) {
         var dd = (IndDatatypeDecl)d;
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
@@ -441,7 +441,7 @@ public virtual Statement CloneStmt(Statement stmt, bool isReference) {
       }
 
       Contract.Assert(false);
-      throw new cce.UnreachableException(); // unexpected statement TODO, make all statements inherit from ICloneable.
+      throw new Cce.UnreachableException(); // unexpected statement TODO, make all statements inherit from ICloneable.
     }
 
     public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) {
@@ -481,7 +481,7 @@ public CalcStmt.CalcOp CloneCalcOp(CalcStmt.CalcOp op) {
         return new CalcStmt.TernaryCalcOp(CloneExpr(((CalcStmt.TernaryCalcOp)op).Index));
       } else {
         Contract.Assert(false);
-        throw new cce.UnreachableException();
+        throw new Cce.UnreachableException();
       }
     }
 

Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs

@@ -39,7 +39,7 @@ public ApplySuffix(IToken tok, IToken/*?*/ atLabel, Expression lhs, List<ActualB
     : base(tok, lhs) {
     Contract.Requires(tok != null);
     Contract.Requires(lhs != null);
-    Contract.Requires(cce.NonNullElements(args));
+    Contract.Requires(Cce.NonNullElements(args));
     AtTok = atLabel;
     CloseParen = closeParen;
     Bindings = new ActualBindings(args);

Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs

@@ -63,7 +63,7 @@ public enum CoCallResolution {
   void ObjectInvariant() {
     Contract.Invariant(Name != null);
     Contract.Invariant(Receiver != null);
-    Contract.Invariant(cce.NonNullElements(Args));
+    Contract.Invariant(Cce.NonNullElements(Args));
     Contract.Invariant(
       Function == null || TypeApplication_AtEnclosingClass == null ||
       Function.EnclosingClass.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count);
@@ -79,7 +79,7 @@ public FunctionCallExpr(IToken tok, string fn, Expression receiver, IToken openP
     Contract.Requires(tok != null);
     Contract.Requires(fn != null);
     Contract.Requires(receiver != null);
-    Contract.Requires(cce.NonNullElements(args));
+    Contract.Requires(Cce.NonNullElements(args));
     Contract.Requires(openParen != null || args.Count == 0);
     Contract.Ensures(type == null);
   }

Source/DafnyCore/AST/Expressions/Applications/MultiSelectExpr.cs

@@ -10,7 +10,7 @@ public class MultiSelectExpr : Expression, ICloneable<MultiSelectExpr> {
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Array != null);
-    Contract.Invariant(cce.NonNullElements(Indices));
+    Contract.Invariant(Cce.NonNullElements(Indices));
     Contract.Invariant(1 <= Indices.Count);
   }
 
@@ -23,7 +23,7 @@ public MultiSelectExpr(IToken tok, Expression array, List<Expression> indices)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(array != null);
-    Contract.Requires(cce.NonNullElements(indices) && 1 <= indices.Count);
+    Contract.Requires(Cce.NonNullElements(indices) && 1 <= indices.Count);
 
     Array = array;
     Indices = indices;

Source/DafnyCore/AST/Expressions/Collections/DisplayExpression.cs

@@ -7,7 +7,7 @@ public abstract class DisplayExpression : Expression {
   public readonly List<Expression> Elements;
   [ContractInvariantMethod]
   void ObjectInvariant() {
-    Contract.Invariant(cce.NonNullElements(Elements));
+    Contract.Invariant(Cce.NonNullElements(Elements));
   }
 
   protected DisplayExpression(Cloner cloner, DisplayExpression original) : base(cloner, original) {
@@ -16,7 +16,7 @@ protected DisplayExpression(Cloner cloner, DisplayExpression original) : base(cl
 
   public DisplayExpression(IToken tok, List<Expression> elements)
     : base(tok) {
-    Contract.Requires(cce.NonNullElements(elements));
+    Contract.Requires(Cce.NonNullElements(elements));
     Elements = elements;
   }