From 62dfa1d58f91f1ff4283ac00a2efdd1ddb694bf9 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 30 Apr 2018 09:54:26 -0700
Subject: [PATCH] Use sbv version 7.7. Fixes #486.

Also add regression test for #486.
---
 cryptol.cabal                     | 4 ++--
 tests/issues/issue486.icry        | 3 +++
 tests/issues/issue486.icry.stdout | 4 ++++
 3 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 tests/issues/issue486.icry
 create mode 100644 tests/issues/issue486.icry.stdout

diff --git a/cryptol.cabal b/cryptol.cabal
index c3e0cad8..a0c83422 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -58,7 +58,7 @@ library
                        pretty            >= 1.1,
                        process           >= 1.2,
                        random            >= 1.0.1,
-                       sbv               >= 7.0,
+                       sbv               >= 7.7,
                        simple-smt        >= 0.7.1,
                        strict,
                        text              >= 1.1,
@@ -262,5 +262,5 @@ benchmark cryptol-bench
                      , deepseq
                      , directory
                      , filepath
-                     , sbv >= 7.0
+                     , sbv >= 7.7
                      , text
diff --git a/tests/issues/issue486.icry b/tests/issues/issue486.icry
new file mode 100644
index 00000000..a8d0cc25
--- /dev/null
+++ b/tests/issues/issue486.icry
@@ -0,0 +1,3 @@
+:prove \(x:Integer) -> x ^^ integer`{0} == integer`{1}
+:prove \(x:Integer) -> x ^^ integer`{1} == x
+:prove \(x:Integer) -> x ^^ integer`{5} == x * x * x * x * x
diff --git a/tests/issues/issue486.icry.stdout b/tests/issues/issue486.icry.stdout
new file mode 100644
index 00000000..fe6d5f41
--- /dev/null
+++ b/tests/issues/issue486.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Q.E.D.
+Q.E.D.
+Q.E.D.