Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error when parsing counterexamples via SBV #986

Closed
robdockins opened this issue Nov 25, 2020 · 1 comment
Closed

Error when parsing counterexamples via SBV #986

robdockins opened this issue Nov 25, 2020 · 1 comment
Labels
bug Something not working correctly
Milestone
2.11.0

Comments

@robdockins
Copy link
Contributor 

Cryptol> :m PrimeEC
Loading module Cryptol
Loading module PrimeEC
PrimeEC> :set prover=z3
PrimeEC> :safe (\a -> ec_affinify`{17} { x = 1, y = 1, z = a })
Counterexample
cryptol: src/Cryptol/Symbolic/SBV.hs:401:9-37: Non-exhaustive patterns in (vs, [])

The What4 backends don't have this issue, so it's something specific with the SBV interaction.
@robdockins robdockins added the bug Something not working correctly label Nov 25, 2020
@atomb atomb added this to the 2.11.0 milestone Dec 11, 2020
@robdockins robdockins mentioned this issue Jan 25, 2021
Closed
@robdockins
Copy link
Contributor Author

Fixed via #1067

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something not working correctly
Projects
None yet
Milestone
2.11.0
Development

No branches or pull requests
2 participants
@atomb @robdockins