fix: Missing token in translation of proper prefix (#2652)

RELEASE_NOTES.md

@@ -2,6 +2,7 @@
 
 - feat: Support for the `{:opaque}` attibute on `const` (https://github.com/dafny-lang/dafny/pull/2545)
 - feat: Support for plugin-based code actions on the IDE (https://github.com/dafny-lang/dafny/pull/2021)
+- fix: Added missing error reporting position on string prefix check (https://github.com/dafny-lang/dafny/pull/2652)
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
 
 

Source/Dafny/Verifier/Translator.BoogieFactory.cs

@@ -643,9 +643,11 @@ public Bpl.Expr ProperPrefix(Bpl.IToken tok, Bpl.Expr e0, Bpl.Expr e1) {
       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
       Bpl.Expr len0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
       Bpl.Expr len1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
-      return Bpl.Expr.And(
+      var result = Bpl.Expr.And(
         Bpl.Expr.Lt(len0, len1),
         FunctionCall(tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0));
+      result.tok = tok;
+      return result;
     }
 
     Bpl.Expr ArrayLength(Bpl.IToken tok, Bpl.Expr arr, int totalDims, int dim) {

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

@@ -0,0 +1,8 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method z(x: string, y: string) {
+  var a: string := "abc";
+  var b: string := x + y;
+  assert a <= x ==> a < b; // SHOULD FAIL
+}

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

@@ -0,0 +1,3 @@
+git-issue-2651.dfy(7,22): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 1 error