Fix: Support for double constant initialization in Dafny-to-Rust

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy

@@ -3361,9 +3361,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
                     rhs]);
                 newEnv := newEnv.RemoveAssigned(isAssignedVar);
               } else {
-                error := Some("Unespected field to assign whose isAssignedVar is not in the environment: " + isAssignedVar);
-                generated :=
-                  R.AssignMember(R.RawExpr(error.value), fieldName, rhs);
+                // Already assigned, safe to override
+                generated := R.Assign(Some(R.SelectMember(modify_macro.Apply1(thisInConstructor), fieldName)), rhs);
               }
             case _ =>
               if onExpr != R.Identifier("self") {

Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

@@ -2834,8 +2834,7 @@ public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, DCOMP._ISelfInfo
                   generated = (((RAST.__default.dafny__runtime).MSel((this).update__field__uninit__macro)).AsExpr()).Apply(Dafny.Sequence<RAST._IExpr>.FromElements((this).thisInConstructor, RAST.Expr.create_Identifier(_4_fieldName), RAST.Expr.create_Identifier(_8_isAssignedVar), rhs));
                   newEnv = (newEnv).RemoveAssigned(_8_isAssignedVar);
                 } else {
-                  (this).error = Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Unespected field to assign whose isAssignedVar is not in the environment: "), _8_isAssignedVar));
-                  generated = RAST.__default.AssignMember(RAST.Expr.create_RawExpr((this.error).dtor_value), _4_fieldName, rhs);
+                  generated = RAST.Expr.create_Assign(Std.Wrappers.Option<RAST._IAssignLhs>.create_Some(RAST.AssignLhs.create_SelectMember(((this).modify__macro).Apply1((this).thisInConstructor), _4_fieldName)), rhs);
                 }
                 goto after_match1;
               }
@@ -5670,7 +5669,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv
                       goto after__ASSIGN_SUCH_THAT_0;
                     }
                   }
-                  throw new System.Exception("assign-such-that search produced no value (line 4736)");
+                  throw new System.Exception("assign-such-that search produced no value (line 4735)");
                 after__ASSIGN_SUCH_THAT_0: ;
                   _63_allReadCloned = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(_63_allReadCloned, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("let ")), _64_next), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" = ")), _64_next), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(".clone();\n"));
                   _62_recIdents = Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Difference(_62_recIdents, Dafny.Set<Dafny.ISequence<Dafny.Rune>>.FromElements(_64_next));
@@ -7026,7 +7025,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv
                   goto after__ASSIGN_SUCH_THAT_1;
                 }
               }
-              throw new System.Exception("assign-such-that search produced no value (line 5272)");
+              throw new System.Exception("assign-such-that search produced no value (line 5271)");
             after__ASSIGN_SUCH_THAT_1: ;
               if ((!object.Equals(selfIdent, DCOMP.SelfInfo.create_NoSelf())) && ((_310_next).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_this")))) {
                 RAST._IExpr _311_selfCloned;

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy

@@ -0,0 +1,14 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+class Cl {
+  const c: bool
+  constructor(c: bool) {
+    this.c := c;
+    this.c := c;
+  }
+}
+
+method Main() {
+  var cl := new Cl(false);
+  print cl.c, "\n";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect

@@ -0,0 +1 @@
+false

docs/dev/news/5642.fix

@@ -0,0 +1 @@
+Support for double constant initialization in Dafny-to-Rust