Fix: Error wording closer to semantics

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