Add regression test for #444.

GaloisInc · Nov 21, 2019 · 85bff67 · 85bff67
1 parent 5725d23
commit 85bff67
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 0 deletions.
diff --git a/tests/issues/issue444.icry b/tests/issues/issue444.icry
@@ -0,0 +1,2 @@
+:set prover = yices
+:prove \(x:[32]) -> x!0 ==> x * (x ^^ -1) == 1
diff --git a/tests/issues/issue444.icry.stdout b/tests/issues/issue444.icry.stdout
@@ -0,0 +1,17 @@
+Loading module Cryptol
+
+SBV exception:
+
+*** Data.SBV: Unexpected non-success response from Yices:
+***
+***    Sent      : (define-fun s64 () (_ BitVec 32) (bvmul s63 s63))
+***    Expected  : success
+***    Received  : (error "at line 69, column 35: in bvmul: maximal polynomial degree exceeded")
+***
+***    Exit code : ExitSuccess
+***    Executable: /Users/huffman/.bin/yices-smt2
+***    Options   : --incremental
+***
+***    Reason    : Check solver response for further information. If your code is correct,
+***                please report this as an issue either with SBV or the solver itself!
+
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		:set prover = yices
		:prove \(x:[32]) -> x!0 ==> x * (x ^^ -1) == 1