-
Notifications
You must be signed in to change notification settings - Fork 127
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
Get models in SMTLIB2 format without printing ASSERT
s (Mac specific issue?)
#475
Comments
Huh, I'm realizing now that, for example,
? |
Thanks @gussmith23, Can you please attach the file that produces the incorrect model? Thanks! |
Yup, here you go!
|
And my version info:
|
Seems to work fine for me:
on
Can you rebuild from the main branch? |
Hm, I am on Mac so I used Homebrew. Will that give me the latest version? The same problem is still manifesting. Version info isn't super useful this time:
|
Are you on Apple silicon? What version of macOS? (I have access to an M1, but not until next week) |
I'm on Mac x86 (2018 Macbook Pro) running MacOS 11.7.8. |
Just verified that it works as expected on Ubuntu. So this does seem to be a problem specifically on Mac. Still a significant issue for me b/c I mainly develop on Mac! |
Is it possible to build from source on Mac? I tried the build instructions and ran into an issue immediately, so I defaulted to the Homebrew install instead. It seems, though, that I do need the latest build on Mac. Are there Mac instructions? |
ASSERT
s ASSERT
s (Mac specific issue?)
I think this is fixed now. Please reopen if I've misunderstood. |
Hi all. We're trying to add support for STP to Rosette. One of the main blockers are the
ASSERT
statements that get printed out when the-p
switch is enabled:We need
-p
so that we get the model out (as seen in the second command), but-p
also adds those unnecessaryASSERT
s. Is there an easy way to disable those while still enabling model production?The text was updated successfully, but these errors were encountered: