Fix: Use correct type for map update expression

Source/DafnyCore/Resolver.cs

@@ -15074,7 +15074,8 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont
         ResolveExpression(e.Index, resolutionContext);
         ResolveExpression(e.Value, resolutionContext);
         AddXConstraint(expr.tok, "SeqUpdatable", e.Seq.Type, e.Index, e.Value, "update requires a sequence, map, or multiset (got {0})");
-        expr.Type = e.Seq.Type;
+        var ty = PartiallyResolveTypeForMemberSelection(expr.tok, e.Seq.Type);
+        expr.Type = ty;
 
       } else if (expr is DatatypeUpdateExpr) {
         var e = (DatatypeUpdateExpr)expr;

Source/DafnyDriver/BoogieAffectingOptions/NonZeroExitCodeIfErrorsOption.cs

@@ -0,0 +1,18 @@
+namespace Microsoft.Dafny;
+
+public class NonZeroExitCodeIfErrorsOption : BooleanOption {
+  public static readonly NonZeroExitCodeIfErrorsOption Instance = new();
+  public override object DefaultValue => true;
+  public override string LongName => "nonzero-exit-code-if-errors";
+  public override string ShortName => null;
+  public override string ArgumentName => "boolean";
+
+  public override string Description => @"
+if false then always exit with a 0 exit code, regardless of whether errors are found.
+If true (default) then use the appropriate exit code.".TrimStart();
+
+  public override string PostProcess(DafnyOptions options) {
+    options.CountVerificationErrors = Get(options);
+    return null;
+  }
+}

Source/DafnyDriver/Commands/CommandRegistry.cs

@@ -22,6 +22,7 @@ static class CommandRegistry {
   public static IReadOnlyList<IOptionSpec> CommonOptions = new List<IOptionSpec>(new IOptionSpec[] {
     CoresOption.Instance,
     VerificationTimeLimitOption.Instance,
+    NonZeroExitCodeIfErrorsOption.Instance,
     LibraryOption.Instance,
     ShowSnippetsOption.Instance,
     PluginOption.Instance,

Source/DafnyDriver/DafnyDriver.cs

@@ -93,6 +93,11 @@ static DafnyDriver() {
       "--verification-time-limit=300"
     };
 
+    public static readonly string[] NewDefaultArgumentsForTestingWithErrors =
+      NewDefaultArgumentsForTesting.Concat(new[] {
+        "--nonzero-exit-code-if-errors=false"
+      }).ToArray();
+
     public static int Main(string[] args) {
       int ret = 0;
       var thread = new System.Threading.Thread(

Source/IntegrationTests/LitTests.cs

@@ -100,6 +100,7 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         throw new Exception($"Unsupported OS: {RuntimeInformation.OSDescription}");
       }
 
+      substitutions["%args_0"] = DafnyDriver.NewDefaultArgumentsForTestingWithErrors;
       substitutions["%args"] = DafnyDriver.NewDefaultArgumentsForTesting;
 
       var dafnyReleaseDir = Environment.GetEnvironmentVariable("DAFNY_RELEASE");

Test/git-issues/git-issue-3059.dfy

@@ -0,0 +1,28 @@
+// RUN: %baredafny verify %args_0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type foo = m: map<int, int> | forall n <- m.Keys :: m[n] < 5
+
+function addToFoo(m: foo): foo
+  ensures false
+{
+  m[1 := 7]
+}
+
+type seq0 = s: seq<int> | forall n <- s :: n == 0
+
+function ReplaceInSeq0(s: seq0): seq0
+  requires |s| > 0
+  ensures false
+{
+  s[0 := 1]
+}
+
+type map0 = m: map<int, int> | forall k <- m :: m[k] == 0
+
+function ReplaceInMap0(m: map0): map0
+  requires 0 in m
+  ensures false
+{
+  m[0 := 1]
+}

Test/git-issues/git-issue-3059.dfy.expect

@@ -0,0 +1,7 @@
+git-issue-3059.dfy(9,3): Error: value does not satisfy the subset constraints of 'foo'
+git-issue-3059.dfy(14,9): Error: A postcondition might not hold on this return path.
+git-issue-3059.dfy(16,10): Related location: This is the postcondition that might not hold.
+git-issue-3059.dfy(18,3): Error: value does not satisfy the subset constraints of 'seq0'
+git-issue-3059.dfy(27,3): Error: value does not satisfy the subset constraints of 'map0'
+
+Dafny program verifier finished with 3 verified, 4 errors

docs/dev/news/3059.fix

@@ -0,0 +1 @@
+Use correct type for map update expression