-
Notifications
You must be signed in to change notification settings - Fork 103
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.
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
Uninformative error message SMT solver returned unexpected status 1
#489
Comments
The error it should be reporting is that Your examples can be made to work by using |
That's interesting. My use case is where I have an enum (which will be a processor state) and with each element of the enum I have an irregular list (or vector) of registers.
Then, in some
If I could get the type-system to check these irregular lists of registers, then there would be more type-safety. But it's not necessary. I am currently doing all this without using fancy types. It's fine. |
The following function fails to compile, and terminates with the uninformative error message
SMT solver returned unexpected status 1
using Sail 0.17 (sail @ opam-v2.1.5).Likewise with this variant:
I can understand why this program is rejected (despite there being enough constraints to make the programs work) since the type checker is looking for a singleton kind as argument for
regno(.)
, but it would be nice to have a more informative error message.The text was updated successfully, but these errors were encountered: