Fix: Error wording closer to semantics

Source/Concurrency/YieldingProcDuplicator.cs

@@ -516,7 +516,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 proved"));
         }
       }
 

Source/Core/AbsyCmd.cs

@@ -2556,7 +2556,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
       // assert that unpacked value has the correct constructor
       var assertCmd = new AssertCmd(tok,
         new NAryExpr(tok, new IsConstructor(tok, Constructor.datatypeTypeCtorDecl, Constructor.index),
-          new List<Expr> { rhs })) { Description = new FailureOnlyDescription("The precondition for unpack might not hold") };
+          new List<Expr> { rhs })) { Description = new FailureOnlyDescription("the precondition for unpack could not be proved") };
       cmds.Add(assertCmd);
       // read fields into lhs variables from localRhs
       var assignLhss = lhs.Args.Select(arg => new SimpleAssignLhs(tok, (IdentifierExpr)arg)).ToList<AssignLhs>();

Source/Core/ProofObligationDescription.cs

@@ -11,7 +11,7 @@ namespace Microsoft.Boogie;
 public abstract class ProofObligationDescription {
   /// <summary>
   /// A description of what this proof obligation means when it has been
-  /// successfully proven.
+  /// successfully proved.
   /// </summary>
   public abstract string SuccessDescription { get; }
 
@@ -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 proved";
 
   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 proved";
 
   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 is the precondition that could not be proved";
 
   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 proved 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 is the postcondition that could not be proved";
 
   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 proved 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

@@ -76,10 +76,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 proved
 Execution trace:
     fakeFilename1(3,3): anon0
-fakeFilename1(8,3): Error: This assertion might not hold.
+fakeFilename1(8,3): Error: this assertion could not be proved
 Execution trace:
     fakeFilename1(8,3): anon0
 
@@ -125,12 +125,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 proved
 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 proved
 Execution trace:
     fakeFilename2(3,3): anon0
 
@@ -175,7 +175,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

Test/aitest0/Intervals.bpl.expect

@@ -1,13 +1,13 @@
-Intervals.bpl(64,3): Error: This assertion might not hold.
-Intervals.bpl(75,3): Error: This assertion might not hold.
-Intervals.bpl(94,3): Error: This assertion might not hold.
-Intervals.bpl(140,3): Error: This assertion might not hold.
-Intervals.bpl(151,3): Error: This assertion might not hold.
-Intervals.bpl(202,3): Error: This assertion might not hold.
-Intervals.bpl(240,3): Error: This assertion might not hold.
-Intervals.bpl(252,3): Error: This assertion might not hold.
-Intervals.bpl(263,3): Error: This assertion might not hold.
-Intervals.bpl(285,3): Error: This assertion might not hold.
-Intervals.bpl(307,3): Error: This assertion might not hold.
+Intervals.bpl(64,3): Error: this assertion could not be proved
+Intervals.bpl(75,3): Error: this assertion could not be proved
+Intervals.bpl(94,3): Error: this assertion could not be proved
+Intervals.bpl(140,3): Error: this assertion could not be proved
+Intervals.bpl(151,3): Error: this assertion could not be proved
+Intervals.bpl(202,3): Error: this assertion could not be proved
+Intervals.bpl(240,3): Error: this assertion could not be proved
+Intervals.bpl(252,3): Error: this assertion could not be proved
+Intervals.bpl(263,3): Error: this assertion could not be proved
+Intervals.bpl(285,3): Error: this assertion could not be proved
+Intervals.bpl(307,3): Error: this assertion could not be proved
 
 Boogie program verifier finished with 17 verified, 11 errors

Test/aitest0/Issue25.bpl.expect

@@ -1,5 +1,5 @@
-Issue25.bpl(12,1): Error: A postcondition might not hold on this return path.
-Issue25.bpl(8,1): Related location: This is the postcondition that might not hold.
+Issue25.bpl(12,1): Error: a postcondition could not be proved on this return path
+Issue25.bpl(8,1): Related location: this is the postcondition that could not be proved
 Execution trace:
     Issue25.bpl(11,3): anon0
     Issue25.bpl(12,1): anon2_LoopHead

Test/aitest1/Bound.bpl.expect

@@ -1,4 +1,4 @@
-Bound.bpl(26,3): Error: This assertion might not hold.
+Bound.bpl(26,3): Error: this assertion could not be proved
 Execution trace:
     Bound.bpl(10,1): start
     Bound.bpl(16,1): LoopHead

Test/aitest9/TestIntervals.bpl.expect

@@ -1,5 +1,5 @@
-TestIntervals.bpl(26,3): Error: This assertion might not hold.
-TestIntervals.bpl(71,3): Error: This assertion might not hold.
-TestIntervals.bpl(72,3): Error: This assertion might not hold.
+TestIntervals.bpl(26,3): Error: this assertion could not be proved
+TestIntervals.bpl(71,3): Error: this assertion could not be proved
+TestIntervals.bpl(72,3): Error: this assertion could not be proved
 
 Boogie program verifier finished with 2 verified, 3 errors

Test/aitest9/VarMapFixpoint.bpl.expect

@@ -1,4 +1,4 @@
-VarMapFixpoint.bpl(13,5): Error: This loop invariant might not be maintained by the loop.
+VarMapFixpoint.bpl(13,5): Error: this loop invariant might not be maintained by the loop
 Execution trace:
     VarMapFixpoint.bpl(7,3): start
     VarMapFixpoint.bpl(12,3): LoopHead

Test/bitvectors/bv5.bpl.expect

@@ -1,4 +1,4 @@
-bv5.bpl(12,3): Error: This assertion might not hold.
+bv5.bpl(12,3): Error: this assertion could not be proved
 Execution trace:
     bv5.bpl(7,12): anon0
 

Test/bitvectors/bv6.bpl.expect

@@ -1,4 +1,4 @@
-bv6.bpl(10,3): Error: This assertion might not hold.
+bv6.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     bv6.bpl(7,5): anon0
 

Test/civl/Program4-fail.bpl.expect

@@ -1,5 +1,5 @@
-Program4-fail.bpl(27,1): Error: A postcondition might not hold on this return path.
-Program4-fail.bpl(6,1): Related location: This is the postcondition that might not hold.
+Program4-fail.bpl(27,1): Error: a postcondition could not be proved on this return path
+Program4-fail.bpl(6,1): Related location: this is the postcondition that could not be proved
 Execution trace:
     Program4-fail.bpl(24,3): anon0
     Program4-fail.bpl(37,5): inline$AtomicIncr$0$anon0

Test/civl/assert-not-first-4.bpl.expect

@@ -1,4 +1,4 @@
-assert-not-first-4.bpl(15,5): Error: This gate of FOO might not hold.
+assert-not-first-4.bpl(15,5): Error: this gate of FOO could not be proved
 Execution trace:
     assert-not-first-4.bpl(8,5): anon0
 

Test/civl/chris4.bpl.expect

@@ -1,4 +1,4 @@
-chris4.bpl(13,3): Error: This assertion might not hold.
+chris4.bpl(13,3): Error: this assertion could not be proved
 Execution trace:
     chris4.bpl(12,3): anon0
     chris4.bpl(12,3): anon0_0

Test/civl/chris5.bpl.expect

@@ -1,4 +1,4 @@
-chris5.bpl(7,3): Error: This gate of P might not hold.
+chris5.bpl(7,3): Error: this gate of P could not be proved
 Execution trace:
     chris5.bpl(12,3): anon0
 

Test/civl/chris6.bpl.expect

@@ -1,4 +1,4 @@
-chris6.bpl(11,3): Error: This assertion might not hold.
+chris6.bpl(11,3): Error: this assertion could not be proved
 Execution trace:
     chris6.bpl(11,3): anon0
 

Test/civl/linear/allocator.bpl.expect

@@ -1,4 +1,4 @@
-allocator.bpl(16,3): Error: This assertion might not hold.
+allocator.bpl(16,3): Error: this assertion could not be proved
 Execution trace:
     allocator.bpl(14,5): anon0
 

Test/civl/linear/bug.bpl.expect

@@ -1,4 +1,4 @@
-bug.bpl(15,3): Error: This assertion might not hold.
+bug.bpl(15,3): Error: this assertion could not be proved
 Execution trace:
     bug.bpl(14,3): anon0
 

Test/civl/linear/f1.bpl.expect

@@ -1,4 +1,4 @@
-f1.bpl(35,4): Error: This assertion might not hold.
+f1.bpl(35,4): Error: this assertion could not be proved
 Execution trace:
     f1.bpl(29,6): anon0
 

Test/civl/linear/f2.bpl.expect

@@ -1,4 +1,4 @@
-f2.bpl(26,4): Error: This assertion might not hold.
+f2.bpl(26,4): Error: this assertion could not be proved
 Execution trace:
     f2.bpl(22,4): anon0
 

Test/civl/parallel4.bpl.expect

@@ -1,4 +1,4 @@
-parallel4.bpl(26,3): Error: This assertion might not hold.
+parallel4.bpl(26,3): Error: this assertion could not be proved
 Execution trace:
     parallel4.bpl(24,5): anon0
     parallel4.bpl(24,5): anon0_0

Test/codeexpr/CodeExpr0.bpl.expect

@@ -1,10 +1,10 @@
-CodeExpr0.bpl(17,3): Error: This assertion might not hold.
+CodeExpr0.bpl(17,3): Error: this assertion could not be proved
 Execution trace:
     CodeExpr0.bpl(17,3): anon0
-CodeExpr0.bpl(22,3): Error: This assertion might not hold.
+CodeExpr0.bpl(22,3): Error: this assertion could not be proved
 Execution trace:
     CodeExpr0.bpl(22,3): anon0
-CodeExpr0.bpl(54,3): Error: This assertion might not hold.
+CodeExpr0.bpl(54,3): Error: this assertion could not be proved
 Execution trace:
     CodeExpr0.bpl(54,3): anon0
 

Test/codeexpr/CodeExpr1.bpl.expect

@@ -1,11 +1,11 @@
-CodeExpr1.bpl(46,5): Error: A postcondition might not hold on this return path.
-CodeExpr1.bpl(42,3): Related location: This is the postcondition that might not hold.
+CodeExpr1.bpl(46,5): Error: a postcondition could not be proved on this return path
+CodeExpr1.bpl(42,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     CodeExpr1.bpl(44,3): start
-CodeExpr1.bpl(54,5): Error: This assertion might not hold.
+CodeExpr1.bpl(54,5): Error: this assertion could not be proved
 Execution trace:
     CodeExpr1.bpl(51,3): start
-CodeExpr1.bpl(68,5): Error: This assertion might not hold.
+CodeExpr1.bpl(68,5): Error: this assertion could not be proved
 Execution trace:
     CodeExpr1.bpl(59,3): start
 

Test/commandline/SplitOnEveryAssert.bpl

@@ -16,7 +16,7 @@
 // CHECK:      checking split 10/12, .*
 // CHECK:      checking split 11/12, .*
 // CHECK:      checking split 12/12, .*
-// CHECK-L: SplitOnEveryAssert.bpl(32,5): Error: This assertion might not hold.
+// CHECK-L: SplitOnEveryAssert.bpl(32,5): Error: this assertion could not be proved
 
 procedure Ex() returns (y: int)
   ensures y >= 0;

Test/commandline/noProc.bpl.1.expect

@@ -1,7 +1,7 @@
-noProc.bpl(10,3): Error: This assertion might not hold.
+noProc.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(10,3): anon0
-noProc.bpl(15,3): Error: This assertion might not hold.
+noProc.bpl(15,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(15,3): anon0
 

Test/commandline/noProc.bpl.2.expect

@@ -1,4 +1,4 @@
-noProc.bpl(10,3): Error: This assertion might not hold.
+noProc.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(10,3): anon0
 

Test/commandline/noProc.bpl.3.expect

@@ -1,7 +1,7 @@
-noProc.bpl(10,3): Error: This assertion might not hold.
+noProc.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(10,3): anon0
-noProc.bpl(15,3): Error: This assertion might not hold.
+noProc.bpl(15,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(15,3): anon0
 

Test/datatypes/field_access_verification_error.bpl.expect

@@ -1,22 +1,22 @@
-field_access_verification_error.bpl(13,1): Error: A postcondition might not hold on this return path.
-field_access_verification_error.bpl(9,3): Related location: This is the postcondition that might not hold.
+field_access_verification_error.bpl(13,1): Error: a postcondition could not be proved on this return path
+field_access_verification_error.bpl(9,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     field_access_verification_error.bpl(11,5): anon0
-field_access_verification_error.bpl(21,1): Error: A postcondition might not hold on this return path.
-field_access_verification_error.bpl(17,3): Related location: This is the postcondition that might not hold.
+field_access_verification_error.bpl(21,1): Error: a postcondition could not be proved on this return path
+field_access_verification_error.bpl(17,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     field_access_verification_error.bpl(19,8): anon0
-field_access_verification_error.bpl(34,1): Error: A postcondition might not hold on this return path.
-field_access_verification_error.bpl(28,3): Related location: This is the postcondition that might not hold.
+field_access_verification_error.bpl(34,1): Error: a postcondition could not be proved on this return path
+field_access_verification_error.bpl(28,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     field_access_verification_error.bpl(31,5): anon0
-field_access_verification_error.bpl(43,3): Error: This assertion might not hold.
+field_access_verification_error.bpl(43,3): Error: this assertion could not be proved
 Execution trace:
     field_access_verification_error.bpl(42,11): anon0
-field_access_verification_error.bpl(50,11): Error: The precondition for unpack might not hold
+field_access_verification_error.bpl(50,11): Error: the precondition for unpack could not be proved
 Execution trace:
     field_access_verification_error.bpl(50,11): anon0
-field_access_verification_error.bpl(60,3): Error: This assertion might not hold.
+field_access_verification_error.bpl(60,3): Error: this assertion could not be proved
 Execution trace:
     field_access_verification_error.bpl(59,5): anon0
 

Test/datatypes/t1.bpl.expect

@@ -1,4 +1,4 @@
-t1.bpl(25,3): Error: This assertion might not hold.
+t1.bpl(25,3): Error: this assertion could not be proved
 Execution trace:
     t1.bpl(18,3): anon0
 

Test/extractloops/detLoopExtractNested.bpl.expect

@@ -1,4 +1,4 @@
-(0,0): Error: This assertion might not hold.
+(0,0): Error: this assertion could not be proved
 Execution trace:
     detLoopExtractNested.bpl(12,12): anon0
     detLoopExtractNested.bpl(14,8): anon5_LoopBody

Test/extractloops/t1.bpl.expect

@@ -1,4 +1,4 @@
-(0,0): Error: This assertion might not hold.
+(0,0): Error: this assertion could not be proved
 Execution trace:
     t1.bpl(19,3): anon0
     t1.bpl(24,3): anon3_LoopHead