diff --git a/tests/issues/issue444.icry b/tests/issues/issue444.icry deleted file mode 100644 index e39a0b4b..00000000 --- a/tests/issues/issue444.icry +++ /dev/null @@ -1,2 +0,0 @@ -: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 deleted file mode 100644 index 9e04bda5..00000000 --- a/tests/issues/issue444.icry.stdout +++ /dev/null @@ -1,17 +0,0 @@ -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! -