1 files changed, 18 insertions, 0 deletions
diff --git a/Test/dafny4/Bug133.dfy b/Test/dafny4/Bug133.dfy
new file mode 100644
index 00000000..f7da133e
--- /dev/null
+++ b/Test/dafny4/Bug133.dfy
@@ -0,0 +1,18 @@
+// RUN: %dafny /noNLarith /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Math__div_def_i { 
+	function my_div_pos(x:int, d:int) : int
+		requires d >  0;
+		decreases if x < 0 then (d - x) else x;
+	{
+		if x < 0 then
+			-1 + my_div_pos(x+d, d)
+		else if x < d then
+			0
+		else
+			1 + my_div_pos(x-d, d)
+	} 
+} 
+
+