Z3 error on some inputs

[joom]

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.

[ViRb3]

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