From bc0545bd62afb81a983252b99da63aeaf7100f1e Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 14 Jul 2020 11:31:50 -0700
Subject: [PATCH 1/2] Add the Eq->Cmp superclass relationship to the regression
 test.

---
 tests/regression/superclass.cry         |  5 +++++
 tests/regression/superclass.icry        |  7 +++++--
 tests/regression/superclass.icry.stdout | 21 ++++++++++++++++++++-
 3 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/tests/regression/superclass.cry b/tests/regression/superclass.cry
index 4f676f1e3..7cbc8eb6d 100644
--- a/tests/regression/superclass.cry
+++ b/tests/regression/superclass.cry
@@ -1,3 +1,5 @@
+module superclass where
+
 zeroRing : {a} (Ring a) => a
 zeroRing = zero
 
@@ -27,3 +29,6 @@ recipRound x = trunc (recip x)
 
 compareRound : {a} (Round a) => a -> a -> Bit
 compareRound x y = x < y
+
+eqCmp : {a} (Cmp a) => a -> a -> Bit
+eqCmp x y = x == y
diff --git a/tests/regression/superclass.icry b/tests/regression/superclass.icry
index 7379acbb2..931414166 100644
--- a/tests/regression/superclass.icry
+++ b/tests/regression/superclass.icry
@@ -1,8 +1,11 @@
-:l superclass.cry
+:m superclass
+
+:browse superclass
 
 :t (fromInteger 42 + zero)
 :t (trunc (recip (fromInteger 5)))
 :t (\x -> x < fromInteger (floor (recip x)))
 :t (\x -> x == zero /. x)
 :t (zero == ~zero)
-:t (\x -> toInteger (x + zero))
\ No newline at end of file
+:t (\x -> toInteger (x + zero))
+:t (\x y -> x < y \/ x == y)
diff --git a/tests/regression/superclass.icry.stdout b/tests/regression/superclass.icry.stdout
index da5da4860..0ce9d8188 100644
--- a/tests/regression/superclass.icry.stdout
+++ b/tests/regression/superclass.icry.stdout
@@ -1,6 +1,24 @@
 Loading module Cryptol
 Loading module Cryptol
-Loading module Main
+Loading module superclass
+Symbols
+=======
+
+  Public
+  ------
+
+    compareRound : {a} (Round a) => a -> a -> Bit
+    eqCmp : {a} (Cmp a) => a -> a -> Bit
+    fromIntField : {a} (Field a) => a
+    fromIntIntegral : {a} (Integral a) => a
+    fromIntRound : {a} (Round a) => a
+    recipRound : {a} (Round a) => a -> Integer
+    zeroField : {a} (Field a) => a
+    zeroIntegral : {a} (Integral a) => a
+    zeroLogic : {a} (Logic a) => a
+    zeroRing : {a} (Ring a) => a
+    zeroRound : {a} (Round a) => a
+
 (fromInteger 42 + zero) : {a} (Ring a) => a
 (trunc (recip (fromInteger 5))) : {a} (Round a) => Integer
 (\x -> x < fromInteger (floor (recip x))) : {a} (Round a) =>
@@ -8,3 +26,4 @@ Loading module Main
 (\x -> x == zero /. x) : {a} (Eq a, Field a) => a -> Bit
 (zero == ~zero) : {a} (Eq a, Logic a) => Bit
 (\x -> toInteger (x + zero)) : {a} (Integral a) => a -> Integer
+(\x y -> x < y \/ x == y) : {a} (Cmp a) => a -> a -> Bit

From c2c1ad123121bebbec22cf033f32296cac440f5b Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 14 Jul 2020 12:09:05 -0700
Subject: [PATCH 2/2] Add regression tests for the `ignore-safety` option

---
 tests/regression/ignore-safe.icry        | 26 ++++++++++++++++++++++++
 tests/regression/ignore-safe.icry.stdout | 15 ++++++++++++++
 2 files changed, 41 insertions(+)
 create mode 100644 tests/regression/ignore-safe.icry
 create mode 100644 tests/regression/ignore-safe.icry.stdout

diff --git a/tests/regression/ignore-safe.icry b/tests/regression/ignore-safe.icry
new file mode 100644
index 000000000..40f0057ed
--- /dev/null
+++ b/tests/regression/ignore-safe.icry
@@ -0,0 +1,26 @@
+:set prover-stats = off
+:set show-examples = off
+
+:set ignore-safety = off
+
+:prove (\ (x:Integer) -> 0 < x ==> x < 4 ==> [3,2,1]@x == 3-x)
+:prove (\ (x:[8]) -> x < 4 ==> [3,2,1]@x == 3-x)
+
+:prove (\ (x:Integer) y -> (y == 0) || (y*(x/y) + x%y == x))
+:prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
+
+:prove (\ (x:Integer) -> [0,0,0]@x == 0 )
+:prove (\ (x:Integer) -> []@x == 0 )
+:prove (\ (x:[8]) -> [0,0,0]@x == 0 )
+
+:set ignore-safety = on
+
+:prove (\ (x:Integer) -> 0 < x ==> x < 4 ==> [3,2,1]@x == 3-x)
+:prove (\ (x:[8]) -> x < 4 ==> [3,2,1]@x == 3-x)
+
+:prove (\ (x:Integer) y -> (y == 0) || (y*(x/y) + x%y == x))
+:prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
+
+:prove (\ (x:Integer) -> [0,0,0]@x == 0 )
+:prove (\ (x:Integer) -> []@x == 0 )
+:prove (\ (x:[8]) -> [0,0,0]@x == 0 )
diff --git a/tests/regression/ignore-safe.icry.stdout b/tests/regression/ignore-safe.icry.stdout
new file mode 100644
index 000000000..cd1ae4820
--- /dev/null
+++ b/tests/regression/ignore-safe.icry.stdout
@@ -0,0 +1,15 @@
+Loading module Cryptol
+Counterexample
+Counterexample
+Counterexample
+Counterexample
+Counterexample
+Counterexample
+Counterexample
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.