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

Z3 error on some inputs #15

Closed
joom opened this issue Mar 1, 2022 · 1 comment
Closed

Z3 error on some inputs #15

joom opened this issue Mar 1, 2022 · 1 comment
Labels
bug Something isn't working

Comments

@joom
Copy link
Collaborator

joom commented Mar 1, 2022

Trying to prove i < n |- i + 1 <= n with Z3 gives the error pthread_create(&m_thread_id, NULL, &thread_func, this) == 0.

Also mentioned in cpitclaudel/z3.wasm#2.
@joom joom added the bug Something isn't working label Mar 1, 2022
@joom joom closed this as completed in c8ed5f5 Mar 1, 2022
@ViRb3
Copy link

ViRb3 commented Apr 24, 2022

There are now official bindings of z3 which support threads, so this use case should work. Check cpitclaudel/z3.wasm#6.

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 isn't working
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@joom @ViRb3