Fix: Error wording closer to semantics

This PR is the companion of dafny-lang/dafny#3324
We established numerous times this year that the wording "might not hold" still incorrectly provides the feeling that the postcondition is incorrect. Rather than focusing on whether assertions hold or not,
this PR fixes the status by focusing on the fact that the verifier was not able to prove the assertion.

Source/Concurrency/YieldingProcDuplicator.cs

@@ -517,7 +517,7 @@ private void InjectGate(Action action, CallCmd callCmd, bool assume = false)
         else
         {
           newCmdSeq.Add(CmdHelper.AssertCmd(assertCmd.tok, expr,
-            $"This gate of {action.proc.Name} might not hold."));
+            $"This gate of {action.proc.Name} could not be proven."));
         }
       }
 

Source/Core/ProofObligationDescription.cs

@@ -32,75 +32,75 @@ public abstract class ProofObligationDescription {
 
 public class AssertionDescription : ProofObligationDescription
 {
-  public override string SuccessDescription => "This assertion holds.";
+  public override string SuccessDescription => "this assertion holds";
 
-  public override string FailureDescription => "This assertion might not hold.";
+  public override string FailureDescription => "this assertion could not be proven";
 
   public override string ShortDescription => "assert";
 }
 
 public class PreconditionDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "All preconditions hold for this call.";
+    "all preconditions hold for this call";
 
   public override string FailureDescription =>
-    "A precondition for this call might not hold.";
+    "a precondition for this call could not be proven";
 
   public override string ShortDescription => "precondition";
 }
 
 public class RequiresDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "This precondition holds.";
+    "this precondition holds";
 
   public override string FailureDescription =>
-    "This is the precondition that might not hold.";
+    "this precondition could not be proven";
 
   public override string ShortDescription => "requires";
 }
 
 public class PostconditionDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "All postconditions hold for this return path.";
+    "all postconditions hold for this return path";
 
   public override string FailureDescription =>
-    "A postcondition might not hold on this return path.";
+    "a postcondition could not be proven on this return path";
 
   public override string ShortDescription => "postcondition";
 }
 
 public class EnsuresDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "This postcondition holds.";
+    "this postcondition holds";
 
   public override string FailureDescription =>
-    "This is the postcondition that might not hold.";
+    "this postcondition could not be proven";
 
   public override string ShortDescription => "ensures";
 }
 
 public class InvariantEstablishedDescription : AssertionDescription
 {
   public override string SuccessDescription =>
-    "This loop invariant holds on entry.";
+    "this loop invariant holds on entry";
 
   public override string FailureDescription =>
-    "This loop invariant might not hold on entry.";
+    "this loop invariant could not be proven on entry";
 
   public override string ShortDescription => "invariant established";
 }
 
 public class InvariantMaintainedDescription : AssertionDescription
 {
   public override string SuccessDescription =>
-    "This loop invariant is maintained by the loop.";
+    "this loop invariant is maintained by the loop";
 
   public override string FailureDescription =>
-    "This loop invariant might not be maintained by the loop.";
+    "this loop invariant might not be maintained by the loop";
 
   public override string ShortDescription => "invariant maintained";
 }

Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs

@@ -70,10 +70,10 @@ procedure Bad2(y: int)
     options.VcsCores = 4;
     var engine = ExecutionEngine.CreateWithoutSharedCache(options);
 
-    var expected = @"fakeFilename1(3,3): Error: This assertion might not hold.
+    var expected = @"fakeFilename1(3,3): Error: this assertion could not be proven
 Execution trace:
     fakeFilename1(3,3): anon0
-fakeFilename1(8,3): Error: This assertion might not hold.
+fakeFilename1(8,3): Error: this assertion could not be proven
 Execution trace:
     fakeFilename1(8,3): anon0
 
@@ -119,12 +119,12 @@ procedure Good(y: int)
     await task1Writer.DisposeAsync();
     await task2Writer.DisposeAsync();
     var output = writer.ToString();
-    var expected = @"fakeFilename1(3,3): Error: This assertion might not hold.
+    var expected = @"fakeFilename1(3,3): Error: this assertion could not be proven
 Execution trace:
     fakeFilename1(3,3): anon0
 
 Boogie program verifier finished with 1 verified, 1 error
-fakeFilename2(3,3): Error: This assertion might not hold.
+fakeFilename2(3,3): Error: this assertion could not be proven
 Execution trace:
     fakeFilename2(3,3): anon0
 
@@ -169,7 +169,7 @@ public async Task LoopInvariantDescriptions()
     await engine.ProcessProgram(writer, program1, "fakeFilename");
     await writer.DisposeAsync();
     var output = writer.ToString();
-    var expected = @"fakeFilename(10,5): Error: This loop invariant might not be maintained by the loop.
+    var expected = @"fakeFilename(10,5): Error: this loop invariant might not be maintained by the loop
 fakeFilename(10,5): Related message: fake failure
 Execution trace:
     fakeFilename(5,3): entry