Test case for issue #662

tests/issues/issue662.cry

@@ -0,0 +1,24 @@
+type Q = (Integer, Integer)
+
+toQ : Integer -> Integer -> Q
+toQ a b =
+  if b == 0 then error "divide by 0" else
+  if b < 0 then (negate a, negate b) else (a, b)
+
+leQ : Q -> Q -> Bit
+leQ (a,b) (c,d) = a*d <= b*c
+
+intToQ : Integer -> Q
+intToQ x = (x, 1)
+
+abs : Integer -> Integer
+abs x = if x < 0 then negate x else x
+
+property divRoundsDown (x : Integer) (y : Integer) =
+  y == 0 \/ leQ (intToQ ( x / y )) (toQ x y)
+
+property divEuclidean (x : Integer) (y : Integer) =
+  y == 0 \/ y * (x / y) + x % y == x
+
+property modAbs (x : Integer) (y : Integer) =
+  y == 0 \/ abs (x % y) < abs y

tests/issues/issue662.icry

@@ -0,0 +1,7 @@
+:l issue662.cry
+
+:set tests=1000
+:check
+
+:set prover=z3
+:prove

tests/issues/issue662.icry.stdout

@@ -0,0 +1,15 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property divRoundsDown Using random testing.
+Testing... Passed 1000 tests.
+property divEuclidean Using random testing.
+Testing... Passed 1000 tests.
+property modAbs Using random testing.
+Testing... Passed 1000 tests.
+:prove divRoundsDown
+	Q.E.D.
+:prove divEuclidean
+	Q.E.D.
+:prove modAbs
+	Q.E.D.