GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-24 16:31:34 +03:00
Code Issues Projects Releases Wiki Activity

Revert "Add regression test for #444."

Browse Source 
This reverts commit 85bff672ef.

The error message in the expected output file `issue444.icry.stdout`
contained a system-specific absolute file path.

Fixes #673.
This commit is contained in:
Brian Huffman 2019-12-16 14:04:07 -08:00
parent ce6f1edd24
commit 3281e7c121
2 changed files with 0 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/issues/issue444.icry
View File

@ -1,2 +0,0 @@
:set prover = yices
:prove \(x:[32]) -> x!0 ==> x * (x ^^ -1) == 1

17
tests/issues/issue444.icry.stdout
View File

@ -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!