1 files changed, 20 insertions, 0 deletions
diff --git a/Test/dafny4/Juggernaut.dfy b/Test/dafny4/Juggernaut.dfy
new file mode 100644
index 00000000..783f725b
--- /dev/null
+++ b/Test/dafny4/Juggernaut.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Jug()
+{
+  var x, y, z;
+  while x > 0 && y > 0 && z > 0
+    decreases x < y, z
+  {
+    if y > x {
+      y := z;
+      x := *;
+      z := x - 1;
+    } else {
+      z := z - 1;
+      x := *;
+      y := x - 1;
+    }
+  }
+}