From a59b15d4e0a8e21d6e266fd8e778bcdac285b1c9 Mon Sep 17 00:00:00 2001
From: alex28sh <alex.shefer.31@gmail.com>
Date: Fri, 12 Jul 2024 15:29:54 +0200
Subject: [PATCH] Nagini Converting

---
 CODE_OF_CONDUCT.md                            |   0
 CONTRIBUTING.md                               |   0
 DAFNY.ORG.txt                                 |   0
 INSTALL.md                                    |   0
 LICENSE.txt                                   |   0
 Makefile                                      |   0
 NOTICES.txt                                   |   0
 README.md                                     |   0
 RELEASE_NOTES.md                              |   0
 SECURITY.md                                   |   0
 Scripts/quicktest.sh                          |   1 +
 Source/Dafny.sln                              |  38 ++
 .../Statements/Assignment/LocalVariable.cs    |  10 +-
 Source/DafnyCore/AST/Types/UserDefinedType.cs |   2 +-
 .../Backends/CSharp/CsharpCodeGenerator.cs    |   3 +-
 .../Backends/Cplusplus/CppCodeGenerator.cs    |   2 +-
 .../Backends/Dafny/DafnyCodeGenerator.cs      |   6 +-
 .../Backends/GoLang/GoCodeGenerator.cs        |   6 +-
 .../Backends/Java/JavaCodeGenerator.cs        |   3 +-
 .../JavaScript/JavaScriptCodeGenerator.cs     |   3 +-
 .../Backends/Python/PythonCodeGenerator.cs    | 355 ++++++++++++++++--
 .../SinglePassCodeGenerator.Expression.cs     |  26 +-
 .../SinglePassCodeGenerator.Statement.cs      |  58 ++-
 .../SinglePassCodeGenerator.cs                |  53 ++-
 Source/DafnyCore/DafnyCore.csproj             |  12 +-
 .../Legacy/SynchronousCliCompilation.cs       |  20 +
 customBoogie.patch                            |   0
 dotnet-tools.json                             |   0
 28 files changed, 518 insertions(+), 80 deletions(-)
 mode change 100644 => 100755 CODE_OF_CONDUCT.md
 mode change 100644 => 100755 CONTRIBUTING.md
 mode change 100644 => 100755 DAFNY.ORG.txt
 mode change 100644 => 100755 INSTALL.md
 mode change 100644 => 100755 LICENSE.txt
 mode change 100644 => 100755 Makefile
 mode change 100644 => 100755 NOTICES.txt
 mode change 100644 => 100755 README.md
 mode change 100644 => 100755 RELEASE_NOTES.md
 mode change 100644 => 100755 SECURITY.md
 mode change 100644 => 100755 customBoogie.patch
 mode change 100644 => 100755 dotnet-tools.json

diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
old mode 100644
new mode 100755
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
old mode 100644
new mode 100755
diff --git a/DAFNY.ORG.txt b/DAFNY.ORG.txt
old mode 100644
new mode 100755
diff --git a/INSTALL.md b/INSTALL.md
old mode 100644
new mode 100755
diff --git a/LICENSE.txt b/LICENSE.txt
old mode 100644
new mode 100755
diff --git a/Makefile b/Makefile
old mode 100644
new mode 100755
diff --git a/NOTICES.txt b/NOTICES.txt
old mode 100644
new mode 100755
diff --git a/README.md b/README.md
old mode 100644
new mode 100755
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
old mode 100644
new mode 100755
diff --git a/SECURITY.md b/SECURITY.md
old mode 100644
new mode 100755
diff --git a/Scripts/quicktest.sh b/Scripts/quicktest.sh
index ae8053131..22328f6a9 100755
--- a/Scripts/quicktest.sh
+++ b/Scripts/quicktest.sh
@@ -63,6 +63,7 @@ $DAFNY build -t:go c.dfy | diff - $tmp || exit 1
 ./c | diff - $tmpx || exit 1
 (cd c-go; GO111MODULE=auto GOPATH=`pwd` go run src/c.go) | diff - $tmpx || exit 1
 echo Building with Python
+echo $DAFNY
 $DAFNY build -t:py c.dfy | diff - $tmp || exit 1
 python c-py/c.py | diff - $tmpx || exit 1
 echo Building with Rust
diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index 23297b185..fc8e8b1fa 100644
--- a/Source/Dafny.sln
+++ b/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
diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
index e90f93964..27967d8e1 100644
--- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
+++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
@@ -80,8 +80,14 @@ public string AssignUniqueName(FreshIdGenerator generator) {
     sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
 
   string compileName;
-  public string CompileName =>
-    compileName ??= SanitizedName;
+  public string CompileName {
+    get {
+      return compileName ??= SanitizedName;
+    }
+    set {
+      compileName = value;
+    }
+  }
 
   // TODO rename and update comment? Or make it nullable?
   public readonly Type SyntacticType;  // this is the type mentioned in the declaration, if any
diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs
index cc97c154d..0c07f4dca 100644
--- a/Source/DafnyCore/AST/Types/UserDefinedType.cs
+++ b/Source/DafnyCore/AST/Types/UserDefinedType.cs
@@ -17,7 +17,7 @@ void ObjectInvariant() {
   }
 
   public readonly Expression NamePath;  // either NameSegment or ExprDotName (with the inner expression satisfying this same constraint)
-  public readonly string Name;
+  public string Name;
   [Rep]
 
   public string FullName {
diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
index 99f4c54c6..5bb11910b 100644
--- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -2046,7 +2046,7 @@ protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, Concre
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       wr.Write($"for ({TypeName(loopIndex.Type, wr, tok)} {loopIndex.CompileName} = ");
       var startWr = wr.Fork();
@@ -2062,6 +2062,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         bodyWr.WriteLine($"{loopIndex.CompileName}--;");
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;
diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
index be83d5f91..cafab1769 100644
--- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
@@ -1324,7 +1324,7 @@ protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyn
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       throw new UnsupportedFeatureException(tok, Feature.ForLoops, "for loops have not yet been implemented");
     }
 
diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
index 0bb731ae3..283cb475a 100644
--- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
@@ -1170,15 +1170,17 @@ protected override ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) {
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       AddUnsupportedFeature(tok, Feature.ForLoops);
+      annotWriter = null;
       return wr;
     }
 
-    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       if (wr is BuilderSyntaxTree<StatementContainer> statementContainer) {
         var whileBuilder = statementContainer.Builder.While();
         guardWriter = new BuilderSyntaxTree<ExprContainer>(whileBuilder, this);
+        annotWriter = guardWriter.Fork();
         return new BuilderSyntaxTree<StatementContainer>(whileBuilder, this);
       } else {
         throw new InvalidOperationException();
diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
index a8007611a..3bc244d7f 100644
--- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -2065,15 +2065,16 @@ protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyn
       }
     }
 
-    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       wr.Write("for ");
       guardWriter = wr.Fork();
       var wBody = wr.NewBlock("");
+      annotWriter = wr.Fork();
       return wBody;
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       wr.Write($"for {loopIndex.CompileName} := ");
       var startWr = wr.Fork();
@@ -2109,6 +2110,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;
diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
index 8fd4afa98..c210b59c4 100644
--- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
@@ -3823,7 +3823,7 @@ protected override ConcreteSyntaxTree CreateForLoop(string indexVar, Action<Conc
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       var nativeType = AsNativeType(loopIndex.Type);
 
@@ -3865,6 +3865,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;
diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
index e2e71971c..a6d381e8d 100644
--- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
@@ -1242,7 +1242,7 @@ protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, Concre
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       var nativeType = AsNativeType(loopIndex.Type);
 
@@ -1280,6 +1280,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;
diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
index 81e3a5b72..deaa44614 100644
--- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
@@ -45,12 +45,12 @@ public PythonCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(
     private const string DafnyDefaultModule = "module_";
     private const string DafnySystemModule = "System_";
     private static readonly ISet<string> DafnyRuntimeGeneratedModuleNames = new HashSet<string> { DafnySystemModule, };
-    const string DafnySetClass = $"{DafnyRuntimeModule}.Set";
+    const string DafnySetClass = "set";
     const string DafnyMultiSetClass = $"{DafnyRuntimeModule}.MultiSet";
-    const string DafnySeqClass = $"{DafnyRuntimeModule}.Seq";
-    private string DafnySeqMakerFunction => UnicodeCharEnabled ? $"{DafnyRuntimeModule}.SeqWithoutIsStrInference" : DafnySeqClass;
-    const string DafnyArrayClass = $"{DafnyRuntimeModule}.Array";
-    const string DafnyMapClass = $"{DafnyRuntimeModule}.Map";
+    const string DafnySeqClass = "list";
+    private string DafnySeqMakerFunction => "list";
+    const string DafnyArrayClass = "list";
+    const string DafnyMapClass = "dict";
     const string DafnyDefaults = $"{DafnyRuntimeModule}.defaults";
     string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
       Contract.Requires(tp is TypeParameter or AbstractTypeDecl);
@@ -615,6 +615,89 @@ private ConcreteSyntaxTree CreateGetter(string name, Type resultType, IToken tok
       return methodWriter.NewBlockPy(header: $"def {name}({(isStatic ? "instance" : "self")}):");
     }
 
+    protected override void GenerateAccessInv(string name, Type type, string prefix, List<string> suffixes, ConcreteSyntaxTree wr) {
+      string typeStr = "";
+      switch (type) {
+        case UserDefinedType udt:
+          if (udt.Name.StartsWith("array")) {
+            typeStr = "list";
+          } else {
+            return;
+          }
+          break;
+        case MapType _:
+          typeStr = "dict";
+          break;
+        case SeqType _:
+          typeStr = "list";
+          break;
+        case SetType _:
+          typeStr = "set";
+          break;
+        default:
+          return;
+          break;
+      }
+      wr.Write(prefix + "(");
+      for (var t = 0; t < suffixes.Count; t++) {
+        wr.Write("Forall(");
+        if (t == 0) {
+          wr.Write(name + suffixes[t]);
+        } else {
+          wr.Write(name + $"{t - 1}" + suffixes[t]);
+        }
+        wr.Write($", lambda {name}{t}: ");
+      }
+      wr.Write("Acc(" + typeStr + "_pred" + "(");
+      if (suffixes.Count == 0) {
+        wr.Write(name);
+      } else {
+        wr.Write(name + $"{suffixes.Count - 1}");
+      }
+      wr.WriteLine(string.Concat(Enumerable.Repeat(")", suffixes.Count + 3)));
+      switch (type) {
+        case UserDefinedType udt: {
+            if (udt.Name.StartsWith("array")) {
+              suffixes.Add("");
+              var numStr = udt.Name.Substring(5, udt.Name.Length - 5);
+              var num = 1;
+              if (numStr != "") {
+                num = Int32.Parse(numStr);
+              }
+              if (num == 1) {
+                GenerateAccessInv(name, udt.TypeArgs[0], prefix, suffixes, wr);
+              } else {
+                udt.Name = $"array{num - 1}";
+                GenerateAccessInv(name, udt, prefix, suffixes, wr);
+              }
+            }
+            break;
+          }
+        case MapType _: {
+            suffixes.Add(".keys()");
+            GenerateAccessInv(name, ((MapType)type).Domain, prefix, suffixes, wr);
+            suffixes.RemoveAt(0);
+            suffixes.Add(".values()");
+            GenerateAccessInv(name, ((MapType)type).Range, prefix, suffixes, wr);
+            break;
+          }
+        case SeqType sqt:
+        case SetType set: {
+            suffixes.Add("");
+            GenerateAccessInv(name, ((CollectionType)type).Arg, prefix, suffixes, wr);
+            break;
+          }
+        default:
+          break;
+      }
+    }
+
+    protected override void EmitOldExpr(Expression e, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
+      wr.Write("Old(");
+      EmitExpr(e, inLetExprBody, wr, wStmt);
+      wr.Write(")");
+    }
+
     private ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody,
         ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody) {
       var customReceiver = !forBodyInheritance && NeedsCustomReceiver(m);
@@ -623,7 +706,74 @@ private ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiation
       wr.Write($"def {protectedName}(");
       var sep = "";
       WriteFormals(ForTypeDescriptors(typeArgs, m.EnclosingClass, m, lookasideBody), m.Ins, m.IsStatic, customReceiver, ref sep, wr);
-      var body = wr.NewBlockPy("):", close: BlockStyle.Newline);
+      Console.WriteLine($"AAAAA METHOD {protectedName}");
+      list_decls.Clear();
+      foreach (var f in m.Ins) {
+        // Console.WriteLine(FormalName(f, 0));
+        // Console.WriteLine(f.Type);
+        switch (f.Type) {
+          case UserDefinedType udt:
+            if (udt.Name.StartsWith("array")) {
+              list_decls.Push((FormalName(f, 0), f.Type));
+            }
+            break;
+          case MapType _:
+          case SeqType _:
+          case SetType _:
+            list_decls.Push((FormalName(f, 0), f.Type));
+            break;
+          default:
+            break;
+        }
+      }
+      var nameRes = "";
+      var ExistsOut = false;
+      wr.Write(")");
+
+      if (m.Outs.Count > 0) {
+        var res = m.Outs[0];
+        wr.Write(" -> ");
+        ExistsOut = true;
+        nameRes = FormalName(res, 0);
+        wr.Write($"{ConvertTypeToPython(res.Type)}");
+      } else {
+        wr.Write(" -> None");
+      }
+      // WriteFormals("", m.Outs, wr);
+      wr.Write(":");
+
+      var body = wr.NewBlockPy("", open: BlockStyle.Newline, close: BlockStyle.Newline);
+
+      foreach (var (name, type) in list_decls) {
+        GenerateAccessInv(name, type, "Requires", new List<string>(), body);
+      }
+
+      foreach (AttributedExpression req in m.Req) {
+        body.Write("Requires(");
+        var t = body.Fork();
+        EmitExpr(req.E, false, body, t);
+        body.WriteLine(")");
+      }
+
+      foreach (var (name, type) in list_decls) {
+        GenerateAccessInv(name, type, "Ensures", new List<string>(), body);
+      }
+
+      if (m.Outs.Count > 0) {
+        GenerateAccessInv("Result()", m.Outs[0].Type, "Ensures", new List<string>(), body);
+      }
+
+      foreach (AttributedExpression ens in m.Ens) {
+        body.Write("Ensures(");
+        var t = body.Fork();
+        if (ExistsOut) {
+          replacedVar = nameRes;
+          needReplacement = true;
+        }
+        EmitExpr(ens.E, false, body, t);
+        needReplacement = false;
+        body.WriteLine(")");
+      }
       if (createBody) {
         if (m.Body.Body.All(s => s.IsGhost)) {
           body.WriteLine("pass");
@@ -666,8 +816,9 @@ private ConcreteSyntaxTree CreateFunction(string name, List<TypeArgumentInstanti
       var protectedName = !forBodyInheritance ? CompanionMemberIdName(member) : IdName(member);
       wr.Write($"def {protectedName}(");
       var sep = "";
+      Console.WriteLine("AAAAA FunCTION");
       WriteFormals(ForTypeDescriptors(typeArgs, member.EnclosingClass, member, lookasideBody), formals, isStatic, customReceiver, ref sep, wr);
-      return wr.NewBlockPy("):", close: BlockStyle.Newline);
+      return wr.NewBlockPy($") -> {ConvertTypeToPython(resultType)} :", close: BlockStyle.Newline);
     }
 
     // Unlike the other compilers, we use lambdas to model type descriptors here.
@@ -792,6 +943,14 @@ private string FullName(TopLevelDecl decl) {
       return string.Join('.', segments);
     }
 
+    private string repeatDimensions(string rangeDefaultValue, int Dims, List<string> dimensions) {
+      if (Dims == 0) {
+        return $"{rangeDefaultValue}";
+      } else {
+        return $"[{repeatDimensions(rangeDefaultValue, Dims - 1, dimensions)}] * {dimensions[dimensions.Count() - Dims]}";
+      }
+    }
+
     protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok,
         bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
 
@@ -819,8 +978,10 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
             var wrString = new ConcreteSyntaxTree();
             StringLiteralWrapper(wrString).Write("\"\"");
             return wrString.ToString();
+          } else if (xType is SeqType) {
+            return $"{TypeHelperName(xType)}([{TypeInitializationValue(type.TypeArgs[0], wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors)}] * 0)"; // TypeInitializationValue
           } else {
-            return $"{TypeHelperName(xType)}({{}})";
+            return $"{TypeHelperName(xType)}([{TypeInitializationValue(type.TypeArgs[0], wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors)}] * 0)";
           }
         case UserDefinedType udt: {
             var cl = udt.ResolvedClass;
@@ -834,15 +995,16 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
                     if (ArrowType.IsPartialArrowTypeName(td.Name)) {
                       return "None";
                     }
+                    var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, usePlaceboValue,
+                      constructTypeParameterDefaultsFromTypeDescriptors);
                     if (td is NonNullTypeDecl decl) {
                       if (decl.Class is ArrayClassDecl arr) {
-                        return $"{DafnyArrayClass}(None, {Enumerable.Repeat("0", arr.Dims).Comma()})";
+                        return repeatDimensions(rangeDefaultValue, arr.Dims, new List<string>(Enumerable.Repeat("0", arr.Dims)));
+                        // return $"{DafnyArrayClass}([{rangeDefaultValue}] * {Enumerable.Repeat("0", arr.Dims).Comma()})";
                       }
                       return "None";
                     }
                     Contract.Assert(udt.TypeArgs.Any() && ArrowType.IsTotalArrowTypeName(td.Name));
-                    var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, usePlaceboValue,
-                      constructTypeParameterDefaultsFromTypeDescriptors);
                     // The final TypeArg contains the result type
                     var arguments = udt.TypeArgs.SkipLast(1).Comma((_, i) => idGenerator.FreshId("x"));
                     return $"(lambda {arguments}: {rangeDefaultValue})";
@@ -921,18 +1083,72 @@ protected override void TypeArgDescriptorUse(bool isStatic, bool lookasideBody,
 
     protected override bool DeclareFormal(string prefix, string name, Type type, IToken tok, bool isInParam, ConcreteSyntaxTree wr) {
       if (isInParam) {
-        wr.Write($"{prefix}{name}");
+        wr.Write($"{prefix}{name} : {ConvertTypeToPython(type)}");
         return true;
       } else {
         return false;
       }
     }
 
+    protected string ConvertTypesToPython(List<Type> typeArgs) {
+      if (typeArgs != null && typeArgs.Count > 0) {
+        return string.Format("[{0}]", Util.Comma(typeArgs, ty => ConvertTypeToPython(ty)));
+      }
+      return "";
+    }
+
+    protected string ConvertTypeToPython(Type type) {
+      switch (type) {
+        case SeqType seqType:
+          return "List" + ConvertTypesToPython(seqType.TypeArgs);
+          break;
+        case SetType setType:
+          return "Set" + ConvertTypesToPython(setType.TypeArgs);
+          break;
+        case RealType realType:
+          return "float";
+          break;
+        case BasicType basicType:
+          return basicType.ToString();
+          break;
+        case MapType mapType:
+          return "Dict" + ConvertTypesToPython(mapType.TypeArgs);
+          break;
+        case UserDefinedType userDefinedType:
+          if (SystemModuleManager.IsTupleTypeName(userDefinedType.Name)) {
+            return "(" + Util.Comma(userDefinedType.TypeArgs, ty => ConvertTypeToPython(ty)) + ")";
+          } else if (userDefinedType.Name.StartsWith("array")) {
+            var numStr = userDefinedType.Name.Substring(5, userDefinedType.Name.Length - 5);
+            var num = 1;
+            if (numStr != "") {
+              num = Int32.Parse(numStr);
+            }
+            return (string.Concat(Enumerable.Repeat("List[", num))) + ConvertTypeToPython(userDefinedType.TypeArgs[0]) + (string.Concat(Enumerable.Repeat("]", num)));
+          } else if (userDefinedType.Name.StartsWith("nat")) {
+            return "int";
+          } else {
+            return userDefinedType.Name + ConvertTypesToPython(userDefinedType.TypeArgs);
+          }
+          break;
+        case IntVarietiesSupertype intVarietiesSupertype:
+          return "int";
+          break;
+        case RealVarietiesSupertype realVarietiesSupertype:
+          return "float";
+          break;
+        case TypeProxy proxy:
+          return ConvertTypeToPython(proxy.T);
+          break;
+        default:
+          throw new NotSupportedException("Not supported type " + type.ToString());
+      }
+    }
+
     protected override void DeclareLocalVar(string name, Type type, IToken tok, bool leaveRoomForRhs, string rhs,
         ConcreteSyntaxTree wr) {
       wr.Write(name);
-      if (type != null) { wr.Write($": {TypeName(type, wr, tok)}"); }
       if (rhs != null) { wr.Write($" = {rhs}"); }
+      if (type != null) { wr.Write($" # type : {ConvertTypeToPython(type)}"); }
       if (!leaveRoomForRhs) {
         wr.WriteLine();
       }
@@ -940,7 +1156,7 @@ protected override void DeclareLocalVar(string name, Type type, IToken tok, bool
 
     protected override ConcreteSyntaxTree DeclareLocalVar(string name, Type type, IToken tok, ConcreteSyntaxTree wr) {
       var w = new ConcreteSyntaxTree();
-      wr.FormatLine($"{name} = {w}");
+      wr.FormatLine($"{name} = {w} # type : {ConvertTypeToPython(type)}");
       return w;
     }
 
@@ -1031,7 +1247,7 @@ protected override ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) {
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       string iterator;
       var lowWr = new ConcreteSyntaxTree();
       string argumentRemainder;
@@ -1044,16 +1260,18 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
       }
       wr.Format($"for {IdName(loopIndex)} in {iterator}({lowWr}{argumentRemainder})");
       var bodyWr = wr.NewBlockPy($":");
+      annotWriter = bodyWr.Fork();
       bodyWr = EmitContinueLabel(labels, bodyWr);
       TrStmtList(body, bodyWr);
 
       return lowWr;
     }
 
-    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       wr.Write("while ");
       guardWriter = wr.Fork();
       var wBody = wr.NewBlockPy(":");
+      annotWriter = wBody.Fork();
       return wBody;
     }
 
@@ -1084,8 +1302,10 @@ protected override string GetQuantifierName(string bvType) {
     protected override ConcreteSyntaxTree CreateForeachLoop(string tmpVarName, Type collectionElementType, IToken tok,
       out ConcreteSyntaxTree collectionWriter, ConcreteSyntaxTree wr) {
       collectionWriter = new ConcreteSyntaxTree();
-      wr.WriteLine($"{tmpVarName}: {TypeName(collectionElementType, wr, tok)}")
-        .Format($"for {tmpVarName} in {collectionWriter}:");
+      DeclareLocalVar(tmpVarName, collectionElementType, tok, false, PlaceboValue(collectionElementType, wr, tok, true), wr);
+      wr.Format($"for {tmpVarName} in {collectionWriter}:");
+      // wr.WriteLine($"{tmpVarName} # type : {collectionElementType}")
+      //   .Format($"for {tmpVarName} in {collectionWriter}:");
       return wr.NewBlockPy();
     }
 
@@ -1112,8 +1332,9 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall, Concre
 
     protected override void EmitNewArray(Type elementType, IToken tok, List<string> dimensions,
       bool mustInitialize, [CanBeNull] string exampleElement, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
-      var initValue = mustInitialize ? DefaultValue(elementType, wr, tok, true) : "None";
-      wr.Write($"{DafnyArrayClass}({initValue}, {dimensions.Comma(s => s)})");
+      var initValue = true ? DefaultValue(elementType, wr, tok, true) : "None";
+      wr.Write(repeatDimensions(initValue, dimensions.Count(), dimensions));
+      // wr.Write($"{DafnyArrayClass}([{initValue}] * {dimensions.Comma(s => s)})");
     }
 
     protected static string TranslateEscapes(string s) {
@@ -1128,11 +1349,11 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
       switch (e) {
         case CharLiteralExpr:
           var escaped = TranslateEscapes((string)e.Value);
-          if (UnicodeCharEnabled) {
-            wr.Write($"{DafnyRuntimeModule}.CodePoint('{escaped}')");
-          } else {
-            wr.Write($"'{escaped}'");
-          }
+          // if (UnicodeCharEnabled) {
+          //   wr.Write($"{DafnyRuntimeModule}.CodePoint('{escaped}')");
+          // } else {
+          wr.Write($"'{escaped}'");
+          // }
           break;
         case StringLiteralExpr str:
           TrStringLiteral(str, StringLiteralWrapper(wr));
@@ -1358,7 +1579,10 @@ protected override void GetSpecialFieldInfo(SpecialField.ID id, object idParam,
         case SpecialField.ID.ArrayLength:
         case SpecialField.ID.ArrayLengthInt:
           var dim = idParam is int d and > 0 ? d : 0;
-          compiledName = $"length({dim})";
+          preString = "len(";
+
+          postString = (string.Concat(Enumerable.Repeat("[0]", dim))) + ")";
+          // compiledName = $"length({dim})";
           break;
         default:
           Contract.Assert(false); // unexpected ID
@@ -1553,11 +1777,24 @@ protected override void EmitDestructor(Action<ConcreteSyntaxTree> source, Formal
       }
     }
 
+    protected override ConcreteSyntaxTree EmitQuantifierExpr(Action<ConcreteSyntaxTree> collection, bool isForall, Type collectionElementType, BoundVar bv, ConcreteSyntaxTree wr) {
+      if (!isForall) {
+        wr.Write("Exists(");
+      } else {
+        wr.Write("Forall(");
+      }
+      collection(wr);
+      wr.Write(", ");
+      var ret = wr.Fork();
+      wr.Write(")");
+      return ret;
+    }
+
     protected override ConcreteSyntaxTree CreateLambda(List<Type> inTypes, IToken tok, List<string> inNames,
         Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, bool untyped = false) {
-      var functionName = ProtectedFreshId("_lambda");
-      wr.Write(functionName);
-      return wStmts.NewBlockPy($"def {functionName}({inNames.Comma()}):", close: BlockStyle.Newline);
+      // var functionName = ProtectedFreshId("_lambda");
+      // wr.Write(functionName);
+      return wr.NewBlockPy($"lambda {inNames.Comma()}:", close: BlockStyle.Nothing);
     }
 
     protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok,
@@ -1887,17 +2124,16 @@ protected override void EmitCollectionDisplay(CollectionType ct, IToken tok, Lis
 
     private static string TypeHelperName(Type ct) {
       return ct switch {
-        SetType => DafnySetClass,
-        SeqType => DafnySeqClass,
-        MapType => DafnyMapClass,
-        MultiSetType => DafnyMultiSetClass,
+        SetType => "set",
+        SeqType => "list",
+        MapType => "dict",
         _ => throw new NotImplementedException()
       };
     }
 
     protected override void EmitMapDisplay(MapType mt, IToken tok, List<ExpressionPair> elements, bool inLetExprBody,
       ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
-      wr.Write($"{DafnyMapClass}({{");
+      wr.Write($"dict({{");
       var sep = "";
       foreach (var p in elements) {
         wr.Write(sep);
@@ -1910,17 +2146,17 @@ protected override void EmitMapDisplay(MapType mt, IToken tok, List<ExpressionPa
     }
 
     protected override void EmitSetBuilder_New(ConcreteSyntaxTree wr, SetComprehension e, string collectionName) {
-      wr.WriteLine($"{collectionName} = {DafnySetClass}()");
+      wr.WriteLine($"{collectionName} = set() # type : {ConvertTypeToPython(e.Type)}");
     }
 
     protected override void EmitMapBuilder_New(ConcreteSyntaxTree wr, MapComprehension e, string collectionName) {
-      wr.WriteLine($"{collectionName} = {DafnyMapClass}()");
+      wr.WriteLine($"{collectionName} = dict() # type : {ConvertTypeToPython(e.Type)}");
     }
 
     protected override void EmitSetBuilder_Add(CollectionType ct, string collName, Expression elmt, bool inLetExprBody,
         ConcreteSyntaxTree wr) {
       var wStmts = wr.Fork();
-      wr.WriteLine($"{collName} = {collName}.union({DafnySetClass}([{Expr(elmt, inLetExprBody, wStmts)}]))");
+      wr.WriteLine($"{collName} = {collName}.union(set([{Expr(elmt, inLetExprBody, wStmts)}]))");
     }
 
     protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IToken tok, string collName, Expression term,
@@ -1952,7 +2188,7 @@ protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok
 
     protected override (Type, Action<ConcreteSyntaxTree>) EmitIntegerRange(Type type, Action<ConcreteSyntaxTree> wLo, Action<ConcreteSyntaxTree> wHi) {
       return (new IntType(), (wr) => {
-        wr.Write($"{DafnyRuntimeModule}.IntegerRange(");
+        wr.Write($"range(");
         wLo(wr);
         wr.Write(", ");
         wHi(wr);
@@ -1961,6 +2197,49 @@ protected override (Type, Action<ConcreteSyntaxTree>) EmitIntegerRange(Type type
       );
     }
 
+    protected override void EmitBoolBoundedPool(bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      wr.Write("([True, False])");
+    }
+
+    protected override void EmitCharBoundedPool(bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      throw new NotImplementedException();
+    }
+
+    protected override void EmitWiggleWaggleBoundedPool(bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      throw new NotImplementedException();
+    }
+
+    protected override void EmitSetBoundedPool(Expression of, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      TrParenExpr(of, wr, inLetExprBody, wStmts);
+      // wr.Write(".Elements" + propertySuffix);
+    }
+
+    protected override void EmitMultiSetBoundedPool(Expression of, bool includeDuplicates, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      wr.Write(includeDuplicates ? "list(" : "set(");
+      TrParenExpr(of, wr, inLetExprBody, wStmts);
+      wr.Write(")");
+    }
+
+    protected override void EmitSubSetBoundedPool(Expression of, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      throw new NotImplementedException();
+    }
+
+    protected override void EmitMapBoundedPool(Expression map, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      TrParenExpr(map, wr, inLetExprBody, wStmts);
+      GetSpecialFieldInfo(SpecialField.ID.Keys, null, null, out var keyName, out _, out _);
+      wr.Write($".{keyName}()");
+    }
+
+    protected override void EmitSeqBoundedPool(Expression of, bool includeDuplicates, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      wr.Write(includeDuplicates ? "list(" : "set(");
+      TrParenExpr(of, wr, inLetExprBody, wStmts);
+      wr.Write(")");
+    }
+
+    protected override void EmitDatatypeBoundedPool(IVariable bv, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      throw new NotImplementedException();
+    }
+
     protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBody, string type,
       ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
       wr.Write("[");
diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs
index 654a5af66..15a4624cd 100644
--- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs
+++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs
@@ -272,9 +272,11 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
             EmitDatatypeValue(dtv, wTypeDescriptorArguments.ToString(), wrArgumentList.ToString(), wr);
             break;
           }
-        case OldExpr:
-          Contract.Assert(false);
-          throw new cce.UnreachableException(); // 'old' is always a ghost
+        case OldExpr oldExpr:
+          EmitOldExpr(oldExpr.E, inLetExprBody, wr, wStmts);
+          break;
+        // Contract.Assert(false);
+        // throw new cce.UnreachableException(); // 'old' is always a ghost
         case UnaryOpExpr opExpr: {
             var e = opExpr;
             if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot) {
@@ -400,17 +402,17 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
                 e.Bounds, e.BoundVars, i);
               wBody = EmitQuantifierExpr(collection, quantifierExpr is ForallExpr, collectionElementType, bv, wBody);
               var native = AsNativeType(e.BoundVars[i].Type);
-              var tmpVarName = ProtectedFreshId(e is ForallExpr ? "_forall_var_" : "_exists_var_");
+              // var tmpVarName = ProtectedFreshId(e is ForallExpr ? "_forall_var_" : "_exists_var_");
               ConcreteSyntaxTree newWBody = CreateLambda(new List<Type> { collectionElementType }, e.tok,
-                new List<string> { tmpVarName }, Type.Bool, wBody, wStmts, untyped: true);
+                new List<string> { IdName(bv) }, Type.Bool, wBody, wStmts, untyped: true);
               wStmts = newWBody.Fork();
-              newWBody = MaybeInjectSubtypeConstraintWrtTraits(
-                tmpVarName, collectionElementType, bv.Type,
-                inLetExprBody, e.tok, newWBody, true, e is ForallExpr);
-              EmitDowncastVariableAssignment(
-                IdName(bv), bv.Type, tmpVarName, collectionElementType, true, e.tok, newWBody);
-              newWBody = MaybeInjectSubsetConstraint(
-                bv, bv.Type, inLetExprBody, e.tok, newWBody, newtypeConversionsWereExplicit, isReturning: true, elseReturnValue: e is ForallExpr);
+              // newWBody = MaybeInjectSubtypeConstraintWrtTraits(
+              //   tmpVarName, collectionElementType, bv.Type,
+              //   inLetExprBody, e.tok, newWBody, true, e is ForallExpr);
+              // EmitDowncastVariableAssignment(
+              //   IdName(bv), bv.Type, tmpVarName, collectionElementType, true, e.tok, newWBody);
+              // newWBody = MaybeInjectSubsetConstraint(
+              //   bv, bv.Type, inLetExprBody, e.tok, newWBody, newtypeConversionsWereExplicit, isReturning: true, elseReturnValue: e is ForallExpr);
               wBody = newWBody;
             }
 
diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
index d6f5f384f..ad863b973 100644
--- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
+++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
@@ -18,6 +18,7 @@
 
 namespace Microsoft.Dafny.Compilers {
   public abstract partial class SinglePassCodeGenerator {
+
     protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts = null) {
       Contract.Requires(stmt != null);
       Contract.Requires(wr != null);
@@ -25,6 +26,14 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
       wStmts ??= wr.Fork();
 
       if (stmt.IsGhost) {
+        switch (stmt) {
+          case AssertStmt assertStmt: {
+              wr.Write($"Assert(");
+              EmitExpr(assertStmt.Expr, false, wr, wStmts);
+              wr.WriteLine(")");
+              break;
+            }
+        }
         return;
       }
       switch (stmt) {
@@ -263,12 +272,26 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               // This loop is allowed to stop iterating at any time. We choose to never iterate, but we still
               // emit a loop structure. The structure "while (false) { }" comes to mind, but that results in
               // an "unreachable code" error from Java, so we instead use "while (true) { break; }".
-              var wBody = CreateWhileLoop(out var guardWriter, wr);
+              var wBody = CreateWhileLoop(out var guardWriter, out var annotWriter, wr);
               EmitExpr(Expression.CreateBoolLiteral(s.Body.tok, true), false, guardWriter, wStmts);
               EmitBreak(null, wBody);
               Coverage.UnusedInstrumentationPoint(s.Body.Tok, "while body");
             } else {
-              var guardWriter = EmitWhile(s.Body.Tok, s.Body.Body, s.Labels, wr);
+              var wBody = CreateWhileLoop(out var guardWriter, out var annotWriter, wr);
+              foreach (var (name, type) in list_decls) {
+                GenerateAccessInv(name, type, "Invariant", new List<string>(), annotWriter);
+              }
+              foreach (AttributedExpression inv in s.Invariants) {
+                annotWriter.Write($"Invariant(");
+                EmitExpr(inv.E, false, annotWriter, wStmts);
+                annotWriter.WriteLine(")");
+              }
+              foreach (Expression ens in s.Decreases.Expressions) {
+                annotWriter.WriteLine($"#decreases {ens}");
+              }
+              wBody = EmitContinueLabel(s.Labels, wBody);
+              Coverage.Instrument(s.Body.Tok, "while body", wBody);
+              TrStmtList(s.Body.Body, wBody);
               EmitExpr(s.Guard, false, guardWriter, wStmts);
             }
 
@@ -279,7 +302,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               Error(ErrorId.c_case_based_loop_forbidden, loopStmt.Tok, "case-based loop forbidden by the --enforce-determinism option", wr);
             }
             if (loopStmt.Alternatives.Count != 0) {
-              var w = CreateWhileLoop(out var whileGuardWriter, wr);
+              var w = CreateWhileLoop(out var whileGuardWriter, out var annotWriter, wr);
               EmitExpr(Expression.CreateBoolLiteral(loopStmt.tok, true), false, whileGuardWriter, wStmts);
               w = EmitContinueLabel(loopStmt.Labels, w);
               foreach (var alternative in loopStmt.Alternatives) {
@@ -308,7 +331,18 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               wStmts = wr.Fork();
               EmitExpr(s.End, false, DeclareLocalVar(endVarName, s.End.Type, s.End.tok, wr), wStmts);
             }
-            var startExprWriter = EmitForStmt(s.Tok, s.LoopIndex, s.GoingUp, endVarName, s.Body.Body, s.Labels, wr);
+            var startExprWriter = EmitForStmt(s.Tok, s.LoopIndex, s.GoingUp, endVarName, s.Body.Body, s.Labels, out var annotWriter, wr);
+            foreach (var (name, type) in list_decls) {
+              GenerateAccessInv(name, type, "Invariant", new List<string>(), annotWriter);
+            }
+            foreach (AttributedExpression inv in s.Invariants) {
+              annotWriter.Write($"Invariant(");
+              EmitExpr(inv.E, false, annotWriter, wStmts);
+              annotWriter.WriteLine(")");
+            }
+            foreach (Expression ens in s.Decreases.Expressions) {
+              annotWriter.WriteLine($"#decreases {ens}");
+            }
             EmitExpr(s.Start, false, startExprWriter, wStmts);
             break;
           }
@@ -443,14 +477,14 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             var i = 0;
             foreach (var local in s.Locals) {
               bool hasRhs = s.Update is AssignSuchThatStmt || s.Update is AssignOrReturnStmt;
-              if (!hasRhs && s.Update is UpdateStmt u) {
-                if (i < u.Rhss.Count && u.Rhss[i] is HavocRhs) {
-                  // there's no specific initial value
-                } else {
-                  hasRhs = true;
-                }
-              }
-              TrLocalVar(local, !hasRhs, wr);
+              // if (!hasRhs && s.Update is UpdateStmt u) {
+              //   if (i < u.Rhss.Count && u.Rhss[i] is HavocRhs) {
+              //     // there's no specific initial value
+              //   } else {
+              //     hasRhs = true;
+              //   }
+              // }
+              TrLocalVar(local, true, wr);
               i++;
             }
             if (s.Update != null) {
diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
index 7ad99fe4a..52d2c4fda 100644
--- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
@@ -83,6 +83,11 @@ int GetUniqueAstNumber(Expression expr) {
       return n;
     }
 
+    protected string replacedVar = "";
+    protected bool needReplacement = false;
+
+    protected Stack<(string, Type)> list_decls = new Stack<(string, Type)>();
+
     public readonly CoverageInstrumenter Coverage;
 
     // Common limits on the size of builtins: tuple, arrow, and array types.
@@ -99,6 +104,7 @@ int GetUniqueAstNumber(Expression expr) {
 
     protected SinglePassCodeGenerator(DafnyOptions options, ErrorReporter reporter) {
       this.Options = options;
+      list_decls = new Stack<(string, Type)>();
       Reporter = reporter;
       Coverage = new CoverageInstrumenter(this);
       System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(GeneratorErrors).TypeHandle);
@@ -382,6 +388,7 @@ protected virtual Type NativeForm(Type type) {
     }
 
     protected abstract bool DeclareFormal(string prefix, string name, Type type, IToken tok, bool isInParam, ConcreteSyntaxTree wr);
+
     /// <summary>
     /// If "leaveRoomForRhs" is false and "rhs" is null, then generates:
     ///     type name;
@@ -626,7 +633,7 @@ protected virtual ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) {
     }
 
     protected virtual ConcreteSyntaxTree EmitWhile(IToken tok, List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {  // returns the guard writer
-      var wBody = CreateWhileLoop(out var guardWriter, wr);
+      var wBody = CreateWhileLoop(out var guardWriter, out var annotWriter, wr);
       wBody = EmitContinueLabel(labels, wBody);
       Coverage.Instrument(tok, "while body", wBody);
       TrStmtList(body, wBody);
@@ -634,12 +641,13 @@ protected virtual ConcreteSyntaxTree EmitWhile(IToken tok, List<Statement> body,
     }
 
     protected abstract ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr);
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr);
 
-    protected virtual ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, ConcreteSyntaxTree wr) {
+    protected virtual ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       wr.Write("while (");
       guardWriter = wr.Fork();
       var wBody = wr.NewBlock(")");
+      annotWriter = wr.Fork();
       return wBody;
     }
 
@@ -1308,6 +1316,8 @@ public enum ResolvedUnaryOp { BoolNot, BitwiseNot, Cardinality }
     protected abstract void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool inLetExprBody,
       ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts);
 
+    protected virtual void EmitOldExpr(Expression e, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { }
+
     protected virtual void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       Type e0Type, Type e1Type, IToken tok, Type resultType,
       out string opString,
@@ -2772,6 +2782,7 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look
         var useReturnStyleOuts = UseReturnStyleOuts(m, nonGhostOutsCount);
         foreach (var p in m.Outs) {
           if (!p.IsGhost) {
+            traceVars(p);
             DeclareLocalOutVar(IdName(p), p.Type, p.tok, PlaceboValue(p.Type, w, p.tok, true), useReturnStyleOuts, w);
           }
         }
@@ -4636,6 +4647,8 @@ protected virtual void TrDividedBlockStmt(Constructor m, DividedBlockStmt divide
     protected virtual void TrStmtList(List<Statement> stmts, ConcreteSyntaxTree writer) {
       Contract.Requires(cce.NonNullElements(stmts));
       Contract.Requires(writer != null);
+      Console.WriteLine(list_decls.Count);
+      var curS = list_decls.Count;
       foreach (Statement ss in stmts) {
         // label:        // if any
         //   <prelude>   // filled via copyInstrWriters -- copies out-parameters used in letexpr to local variables
@@ -4651,6 +4664,9 @@ protected virtual void TrStmtList(List<Statement> stmts, ConcreteSyntaxTree writ
         TrStmt(ss, w);
         copyInstrWriters.Pop();
       }
+      while (list_decls.Count > curS) {
+        list_decls.Pop();
+      }
     }
 
     protected ConcreteSyntaxTree EmitContinueLabel(LList<Label> loopLabels, ConcreteSyntaxTree writer) {
@@ -4661,8 +4677,26 @@ protected ConcreteSyntaxTree EmitContinueLabel(LList<Label> loopLabels, Concrete
       return writer;
     }
 
+    private void traceVars(IVariable v) {
+      switch (v.Type) {
+        case UserDefinedType udt:
+          if (udt.Name.StartsWith("array")) {
+            list_decls.Push((IdName(v), v.Type));
+          }
+          break;
+        case MapType _:
+        case SeqType _:
+        case SetType _:
+          list_decls.Push((IdName(v), v.Type));
+          break;
+        default:
+          break;
+      }
+    }
+
     void TrLocalVar(IVariable v, bool alwaysInitialize, ConcreteSyntaxTree wr) {
       Contract.Requires(v != null);
+      traceVars(v);
       if (v.IsGhost) {
         // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)
         return;
@@ -4710,6 +4744,9 @@ ConcreteSyntaxTree MatchCasePrelude(string source, UserDefinedType sourceType, D
       return w;
     }
 
+    protected virtual void GenerateAccessInv(string name, Type type, string prefix, List<string> suffixes, ConcreteSyntaxTree wr) {
+    }
+
     // ----- Expression ---------------------------------------------------------------------------
 
     /// <summary>
@@ -4763,7 +4800,11 @@ protected ConcreteSyntaxTree CoercedExpr(Expression expr, Type toType, bool inLe
     }
 
     protected virtual void EmitIdentifier(string ident, ConcreteSyntaxTree wr) {
-      wr.Write(ident);
+      if (needReplacement && ident == replacedVar) {
+        wr.Write("Result()");
+      } else {
+        wr.Write(ident);
+      }
     }
 
     public virtual ConcreteSyntaxTree Expr(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wStmts) {
@@ -4986,7 +5027,7 @@ private ConcreteSyntaxTree MaybeInjectSubsetConstraint(IVariable boundVar, Type
           if (isReturning) {
             var elseBranch = wr;
             elseBranch = EmitBlock(elseBranch);
-            elseBranch = EmitReturnExpr(elseBranch);
+            // elseBranch = EmitReturnExpr(elseBranch);
             var wStmts = elseBranch.Fork();
             EmitExpr(Expression.CreateBoolLiteral(tok, elseReturnValue), inLetExprBody, elseBranch, wStmts);
           }
@@ -4995,7 +5036,7 @@ private ConcreteSyntaxTree MaybeInjectSubsetConstraint(IVariable boundVar, Type
       }
 
       if (isReturning) {
-        wr = EmitReturnExpr(wr);
+        // wr = EmitReturnExpr(wr);
       }
       return wr;
     }
diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
index ebf85839d..18bb36fb9 100644
--- a/Source/DafnyCore/DafnyCore.csproj
+++ b/Source/DafnyCore/DafnyCore.csproj
@@ -34,7 +34,17 @@
       <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.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.1.6" />
+      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Graph\Graph.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Model\Model.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCExpr\VCExpr.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCGeneration\VCGeneration.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Provers\SMTLib\SMTLib.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Houdini\Houdini.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency.csproj" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 
diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
index 150a7434a..f1e58cfc3 100644
--- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
+++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
@@ -240,6 +240,8 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
       ReadOnlyCollection<string> otherFileNames,
       DafnyOptions options, ProofDependencyManager depManager,
       bool lookForSnapshots = true, string programId = null) {
+
+      Console.WriteLine("AAAAAAAAAAAAAAAAAAA");
       Contract.Requires(cce.NonNullElements(dafnyFiles));
       var dafnyFileNames = DafnyFile.FileNames(dafnyFiles);
 
@@ -275,6 +277,7 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
       }
 
       string programName = dafnyFileNames.Count == 1 ? dafnyFileNames[0] : "the_program";
+      Console.WriteLine(programName);
       var (dafnyProgram, err) = await DafnyMain.ParseCheck(options.Input, dafnyFiles, programName, options);
       if (err != null) {
         exitValue = ExitValue.DAFNY_ERROR;
@@ -282,6 +285,9 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
       } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck
           && options.DafnyVerify) {
 
+
+        Console.WriteLine(dafnyProgram);
+
         dafnyProgram.ProofDependencyManager = depManager;
         var boogiePrograms =
           await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList());
@@ -673,6 +679,12 @@ public static async Task<bool> CompileDafnyProgram(Program dafnyProgram, string
       {
         var output = new ConcreteSyntaxTree();
 
+        Console.WriteLine(dafnyProgram.MainMethod);
+
+        foreach (KeyValuePair<ModuleDefinition, ModuleSignature> entry in dafnyProgram.ModuleSigs) {
+          Console.WriteLine("Key: {0}, Value: {1}", entry.Key, entry.Value.ModuleDef);
+        }
+
         await DafnyMain.LargeStackFactory.StartNew(() => compiler.Compile(dafnyProgram, dafnyProgramName, output));
 
         var writerOptions = new WriterState();
@@ -690,9 +702,11 @@ public static async Task<bool> CompileDafnyProgram(Program dafnyProgram, string
         }
       }
       string callToMain = null;
+      Console.WriteLine(hasMain);
       if (hasMain) {
         var callToMainTree = new ConcreteSyntaxTree();
         string baseName = Path.GetFileNameWithoutExtension(dafnyProgramName);
+        Console.WriteLine(mainMethod);
         compiler.EmitCallToMain(mainMethod, baseName, callToMainTree);
         callToMain = callToMainTree.MakeString(compiler.TargetIndentSize); // assume there aren't multiple files just to call main
       }
@@ -707,6 +721,12 @@ public static async Task<bool> CompileDafnyProgram(Program dafnyProgram, string
       // blurt out the code to a file, if requested, or if other target-language files were specified on the command line.
       if (options.SpillTargetCode > 0 || otherFileNames.Count > 0 || (invokeCompiler && !compiler.SupportsInMemoryCompilation) ||
           (invokeCompiler && compiler.TextualTargetIsExecutable && !options.RunAfterCompile)) {
+        Console.WriteLine("WriteDafnyProgramToFiles");
+        Console.WriteLine(targetProgramText);
+        foreach (KeyValuePair<string, string> entry in otherFiles) {
+          Console.WriteLine("Key: {0}, Value: {1}", entry.Key, entry.Value);
+        }
+        // Console.WriteLine(otherFiles);
         compiler.CleanSourceDirectory(targetPaths.SourceDirectory);
         WriteDafnyProgramToFiles(options, targetPaths, targetProgramHasErrors, targetProgramText, callToMain, otherFiles, outputWriter);
       }
diff --git a/customBoogie.patch b/customBoogie.patch
old mode 100644
new mode 100755
diff --git a/dotnet-tools.json b/dotnet-tools.json
old mode 100644
new mode 100755