2 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index c94c18d2..dcd41077 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -19,8 +19,8 @@ method M(a: int, b: int, c: int, x: int)
     f(f(a, b), c);
     { assert f(a, b) == x; }
     f(x, c);
-    { assert c <= x; Monotonicity(c, x); }
-    <= f(x, x);
+    <= { assert c <= x; Monotonicity(c, x); }
+    f(x, x);
     { DiagonalIdentity(x); }
     x;
   }
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index d3ff244a..7497618c 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -28,8 +28,8 @@ ghost method lemma_ping(j: nat, n: nat)
       j <= n;
       { lemma_ping(j - 1, n - 1); }
       j - 1 <= f(n - 1);
-      { lemma_ping(j - 1, f(n - 1)); }
-      ==> j - 1 <= f(f(n - 1));
+      ==> { lemma_ping(j - 1, f(n - 1)); }
+      j - 1 <= f(f(n - 1));
       // (0)
       j - 1 <= f(f(n - 1)) && f(f(n - 1)) < f(n);
       ==> j - 1 < f(n);