From d08046d0630ae55c75524a19c90e6e6e96dc73ec Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 2 Apr 2020 09:40:44 -0700
Subject: [PATCH] Test case for issue #662

---
 tests/issues/issue662.cry         | 24 ++++++++++++++++++++++++
 tests/issues/issue662.icry        |  7 +++++++
 tests/issues/issue662.icry.stdout | 15 +++++++++++++++
 3 files changed, 46 insertions(+)
 create mode 100644 tests/issues/issue662.cry
 create mode 100644 tests/issues/issue662.icry
 create mode 100644 tests/issues/issue662.icry.stdout

diff --git a/tests/issues/issue662.cry b/tests/issues/issue662.cry
new file mode 100644
index 000000000..07e625998
--- /dev/null
+++ b/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
diff --git a/tests/issues/issue662.icry b/tests/issues/issue662.icry
new file mode 100644
index 000000000..10ce494ce
--- /dev/null
+++ b/tests/issues/issue662.icry
@@ -0,0 +1,7 @@
+:l issue662.cry
+
+:set tests=1000
+:check
+
+:set prover=z3
+:prove
diff --git a/tests/issues/issue662.icry.stdout b/tests/issues/issue662.icry.stdout
new file mode 100644
index 000000000..3f0641eaa
--- /dev/null
+++ b/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.