1 files changed, 18 insertions, 0 deletions
diff --git a/test/coq/pass/while_MM_terminating.sail b/test/coq/pass/while_MM_terminating.sail
new file mode 100644
index 00000000..e3bca7f5
--- /dev/null
+++ b/test/coq/pass/while_MM_terminating.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+register COUNT : int
+
+register INT : bool
+
+function test () -> unit = {
+  COUNT = 0;
+  while not_bool(INT) do {
+    COUNT = COUNT + 1;
+    if COUNT > 5 then
+      INT = true
+  }
+}
+
+termination_measure test while (5 - COUNT)