Failed to verify: pthread_create(&m_thread_id, NULL, &thread_func, this) == 0

[sim642]

I experimented around with this and with nontrivial examples I'm getting an error:

Failed to verify: pthread_create(&m_thread_id, NULL, &thread_func, this) == 0

Example of code causing that:

(declare-const x00 Int)
(assert (and (<= 0 x00) (< x00 6)))
(declare-const x01 Int)
(assert (and (<= 0 x01) (< x01 6)))
(declare-const x02 Int)
(assert (and (<= 0 x02) (< x02 6)))
(declare-const x03 Int)
(assert (and (<= 0 x03) (< x03 6)))
(declare-const x04 Int)
(assert (and (<= 0 x04) (< x04 6)))
(declare-const x05 Int)
(assert (and (<= 0 x05) (< x05 6)))
(assert (distinct x00 x01 x02 x03 x04 x05))
(declare-const x10 Int)
(assert (and (<= 0 x10) (< x10 6)))
(declare-const x11 Int)
(assert (and (<= 0 x11) (< x11 6)))
(declare-const x12 Int)
(assert (and (<= 0 x12) (< x12 6)))
(declare-const x13 Int)
(assert (and (<= 0 x13) (< x13 6)))
(declare-const x14 Int)
(assert (and (<= 0 x14) (< x14 6)))
(declare-const x15 Int)
(assert (and (<= 0 x15) (< x15 6)))
(assert (distinct x10 x11 x12 x13 x14 x15))
(declare-const x20 Int)
(assert (and (<= 0 x20) (< x20 6)))
(declare-const x21 Int)
(assert (and (<= 0 x21) (< x21 6)))
(declare-const x22 Int)
(assert (and (<= 0 x22) (< x22 6)))
(declare-const x23 Int)
(assert (and (<= 0 x23) (< x23 6)))
(declare-const x24 Int)
(assert (and (<= 0 x24) (< x24 6)))
(declare-const x25 Int)
(assert (and (<= 0 x25) (< x25 6)))
(assert (distinct x20 x21 x22 x23 x24 x25))
(declare-const x30 Int)
(assert (and (<= 0 x30) (< x30 6)))
(declare-const x31 Int)
(assert (and (<= 0 x31) (< x31 6)))
(declare-const x32 Int)
(assert (and (<= 0 x32) (< x32 6)))
(declare-const x33 Int)
(assert (and (<= 0 x33) (< x33 6)))
(declare-const x34 Int)
(assert (and (<= 0 x34) (< x34 6)))
(declare-const x35 Int)
(assert (and (<= 0 x35) (< x35 6)))
(assert (distinct x30 x31 x32 x33 x34 x35))
(declare-const x40 Int)
(assert (and (<= 0 x40) (< x40 6)))
(declare-const x41 Int)
(assert (and (<= 0 x41) (< x41 6)))
(declare-const x42 Int)
(assert (and (<= 0 x42) (< x42 6)))
(declare-const x43 Int)
(assert (and (<= 0 x43) (< x43 6)))
(declare-const x44 Int)
(assert (and (<= 0 x44) (< x44 6)))
(declare-const x45 Int)
(assert (and (<= 0 x45) (< x45 6)))
(assert (distinct x40 x41 x42 x43 x44 x45))
(declare-const x50 Int)
(assert (and (<= 0 x50) (< x50 6)))
(declare-const x51 Int)
(assert (and (<= 0 x51) (< x51 6)))
(declare-const x52 Int)
(assert (and (<= 0 x52) (< x52 6)))
(declare-const x53 Int)
(assert (and (<= 0 x53) (< x53 6)))
(declare-const x54 Int)
(assert (and (<= 0 x54) (< x54 6)))
(declare-const x55 Int)
(assert (and (<= 0 x55) (< x55 6)))
(assert (distinct x50 x51 x52 x53 x54 x55))
(assert (or (= x55 (+ x51 1)) (= x55 (- x51 1))))
(assert (= x33 x42))
(check-sat)

[sim642]

Turns out this is a problem with configuration under emscripten: Z3Prover/z3#1298 (comment).

[rudi-cilibrasi]

Wonder if you think this new effort might help (alternate strategy) ? https://github.com/kripken/emscripten/wiki/Pthreads-with-WebAssembly

[cpitclaudel]

Thanks for the report. It looks like rebuilding with thread support disable should fix this.

[mgree]

I tried building with --single-threaded and had no success running z3.wasm with timeouts. I published a release of that build at https://github.com/mgree/z3.wasm/releases/tag/v0.1.1 if anyone wants to try it.

The error messages I got were obscure. Using -T:2, I got "exception thrown: 5607968"; using -t:2000, I got "exception thrown: 7517160".

[joom]

Has anyone been able to fix this? Here's the smallest case I've got this error on:

(declare-const i Int)
(declare-const n Int)
(assert (not (=> (< i n) (<= (+ i 1) n))))
(check-sat)
(exit)

[frizensami]

I am also facing the same issue, the smallest case I can get (running at https://people.csail.mit.edu/cpitcla/z3.wasm/z3.html) is

(declare-fun y () Int)
(declare-fun x () Int)
(assert (or (= y 1) (= y 2)))
(assert (or (= x 3) (= x 4)))
(check-sat)
(exit)

Failed to verify: pthread_create(&m_thread_id, NULL, &thread_func, this) == 0
-- Verification complete (55ms)

Removing any of the four equalities causes the solver to return sat.

However, this formulation returns sat ((= y 1) changed to (= y 0)):

(declare-fun y () Int)
(declare-fun x () Int)
(assert (or (= y 0) (= y 2)))
(assert (or (= x 3) (= x 4)))
(check-sat)
(exit)

sat
-- Verification complete (56ms)

Not sure what to make of it since I'm not familiar with the internals of Z3 and Emscripten, is there anything significant about the differences between these two examples?

[frizensami]

I found a temporary hack around this. Since my use-case involves optimization, adding a set of declarations such as:

(declare-fun z () Int)
(assert-soft (= z 10))

bypasses this issue. Full working example:

(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun z () Int)
(assert (or (= y 1) (= y 2)))
(assert (or (= x 3) (= x 4)))
(assert-soft (= z 10))
(check-sat)
(exit)

I expect this is due to the solve technique changing completely, which bypasses the pthread creation by extension, so it might tank performance.

[ViRb3]

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

EDIT: I can confirm that all "broken" expressions in this issue work correctly on the official bindings.