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

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

@@ -3398,9 +3398,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

@@ -2855,8 +2855,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;
               }

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