s/loops with/may loop with/

9 files changed, 29 insertions, 29 deletions

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
index 270f7e57..6f5ed3d7 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -2,7 +2,7 @@ loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers:
    {P(y, x)}, {P(x, y)}

 loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers:

    {P(y, x)}, {P(x, y)}

-loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})

+loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})

  (!) Suppressing loops would leave this expression without triggers.

 

 Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
index 72482de5..ce62d868 100644
--- a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
+++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
@@ -1,6 +1,6 @@
-loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)})

+loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})

  (!) Suppressing loops would leave this expression without triggers.

-loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)})

+loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})

  (!) Suppressing loops would leave this expression without triggers.

 

 Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
index 89d7265c..804a0116 100644
--- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -1,21 +1,21 @@
 loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))}

- Rejected triggers: {f(i)} (loops with {f(f(i))})

-loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (loops with {f(i + 1)})

+ Rejected triggers: {f(i)} (may loop with {f(f(i))})

+loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop with {f(i + 1)})

  (!) Suppressing loops would leave this expression without triggers.

-loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (loops with {f(i + 1)})

+loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (may loop with {f(i + 1)})

 loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == f(i + 1)}:

    Selected triggers: {g(i)}

-   Rejected triggers: {f(i)} (loops with {f(i + 1)})

+   Rejected triggers: {f(i)} (may loop with {f(i + 1)})

 loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == g(i)}:

    Selected triggers:

      {g(i)}, {f(i)}

 loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:

-   Selected triggers: {f(i)} (loops with {f(i + 1)})

+   Selected triggers: {f(i)} (may loop with {f(i + 1)})

    (!) Suppressing loops would leave this expression without triggers.

 loop-detection-messages--unit-tests.dfy(16,9): Info: For expression {false ==> f(i) == f(i)}:

    Selected triggers: {f(i)}

 loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i + 1)}:

-   Selected triggers: {f(i)} (loops with {f(i + 1)})

+   Selected triggers: {f(i)} (may loop with {f(i + 1)})

 loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i)}:

    Selected triggers: {f(i)}

 loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}

diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
index c0eebdba..58094110 100644
--- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
@@ -1,10 +1,10 @@
 looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers:

    {h(h(c, j), j)}, {h(c, i)}, {c in sc}

- Rejected triggers: {h(c, j)} (loops with {h(h(c, j), j)})

+ Rejected triggers: {h(c, j)} (may loop with {h(h(c, j), j)})

 looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)}

  Rejected triggers: {g(f(x))} (more specific than {f(x)})

 looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers:

    {old(f(f(c)))}, {f(c)}, {c in sc}

- Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))})

+ Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})

 

 Dafny program verifier finished with 9 verified, 0 errors

diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect
index b9dd1d88..35df02f5 100644
--- a/Test/triggers/matrix-accesses-are-triggers.dfy.expect
+++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect
@@ -1,4 +1,4 @@
-matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (loops with {m[j, i + 1]})

+matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with {m[j, i + 1]})

  (!) Suppressing loops would leave this expression without triggers.

 matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range

 Execution trace:

diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
index 23ec089d..313d7c16 100644
--- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
@@ -2,14 +2,14 @@ old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers:
    {old(f(c))}, {c in sc}

 old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers:

    {old(f(f(c)))}, {f(c)}, {c in sc}

- Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))})

+ Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})

 old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers:

    {f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc}

  Rejected triggers:

-   {g(c)} (loops with {g(f(c))})

-   {f(c)} (loops with {f(g(c))})

-   {old(g(c))} (loops with {old(g(f(c)))})

-   {old(f(c))} (loops with {old(f(f(c)))}, {old(f(g(c)))})

+   {g(c)} (may loop with {g(f(c))})

+   {f(c)} (may loop with {f(g(c))})

+   {old(g(c))} (may loop with {old(g(f(c)))})

+   {old(f(c))} (may loop with {old(f(f(c)))}, {old(f(g(c)))})

 old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers:

    {old(f(c))}, {f(c)}, {c in sc}

  Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))})

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
index 83648626..f5e47454 100644
--- a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -1,10 +1,10 @@
-some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (loops with {s[x + 1]})

+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop with {s[x + 1]})

  (!) Suppressing loops would leave this expression without triggers.

 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:

-   Selected triggers: {s[x]} (loops with {s[x + 1]})

+   Selected triggers: {s[x]} (may loop with {s[x + 1]})

    (!) Suppressing loops would leave this expression without triggers.

 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> x + 2 !in s}:

-   Selected triggers: {s[x]} (loops with {x + 2 !in s})

+   Selected triggers: {s[x]} (may loop with {x + 2 !in s})

    (!) Suppressing loops would leave this expression without triggers.

 

 Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
index 63cbc476..58c8dd2b 100644
--- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -1,11 +1,11 @@
 splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)}

- Rejected triggers: {P(i)} (loops with {P(i + 1)})

+ Rejected triggers: {P(i)} (may loop with {P(i + 1)})

 splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)}

- Rejected triggers: {P(j)} (loops with {P(j + 1)})

+ Rejected triggers: {P(j)} (may loop with {P(j + 1)})

 splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}

- Rejected triggers: {P(i)} (loops with {P(i + 1)})

+ Rejected triggers: {P(i)} (may loop with {P(i + 1)})

 splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)}

- Rejected triggers: {P(j)} (loops with {P(j + 1)})

+ Rejected triggers: {P(j)} (may loop with {P(j + 1)})

 splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}:

    Selected triggers:

      {Q(i)}, {P(i)}

@@ -14,19 +14,19 @@ splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i)
      {Q(i)}, {P(i)}

 splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i + 1)}:

    Selected triggers: {Q(i)}

-   Rejected triggers: {P(i)} (loops with {P(i + 1)})

+   Rejected triggers: {P(i)} (may loop with {P(i + 1)})

 splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}:

    Selected triggers:

      {Q(j)}, {P(j)}

 splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> Q(j) ==> P(j + 1)}:

    Selected triggers: {Q(j)}

-   Rejected triggers: {P(j)} (loops with {P(j + 1)})

+   Rejected triggers: {P(j)} (may loop with {P(j + 1)})

 splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}:

    Selected triggers:

      {P(i)}, {Q(i)}

 splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> P(i) ==> P(i + 1)}:

    Selected triggers:

-     {P(i)} (loops with {P(i + 1)}), {Q(i)}

+     {P(i)} (may loop with {P(i + 1)}), {Q(i)}

 splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.

 splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.

 Execution trace:

diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect
index a526e517..2e9bbedf 100644
--- a/Test/triggers/useless-triggers-are-removed.dfy.expect
+++ b/Test/triggers/useless-triggers-are-removed.dfy.expect
@@ -5,11 +5,11 @@ useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}
    {h(f(x))} (more specific than {f(x)})

    {g(f(x))} (more specific than {f(x)})

 useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}

- Rejected triggers: {f(x)} (loops with {f(f(x))})

+ Rejected triggers: {f(x)} (may loop with {f(f(x))})

 useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:

    {g(f(x)), g(y)}, {f(y), f(x)}

  Rejected triggers:

-   {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))})

+   {g(y), f(x)} (may loop with {g(f(y))}, {g(f(x))})

    {g(f(x)), g(f(y))} (more specific than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})

    {g(f(x)), f(y)} (more specific than {f(y), f(x)})

    {g(f(y)), f(x)} (more specific than {f(y), f(x)})