SAT check on an ite returning an unexpected unknown

[PetarMax]

The script below shows that In Z3 v4.13.4, an ite stalls (the timeout can be increased arbitrarily) but there is enough information for satisfiability to be understood - the condition can be proven to hold and each of the branches can be proven SAT. This started happening after Z3 was upgraded from v4.13.0 to v4.13.4 as part of the formal verification effort at Runtime Verification, Inc.

(set-option :timeout 1000)

(declare-const G Int)
(declare-const I Int)
(declare-const S Int)

(assert (<= 1 G))
(assert (<= 0 I))
(assert (<= 0 S))
(assert (<= (+ (* 52 I) 21) G))

(push)

; This ite times out
(assert (< (+ S (ite (or (= 0 (mod (* I (+ I 1)) 2)) (>= (* I (+ I 1)) 0)) (div (* I (+ I 1)) 2) (ite (> 2 0) (+ (div (* I (+ I 1)) 2) 1) (- (div (* I (+ I 1)) 2) 1)))) 115792089237316195423570985008687907853269984665640564039457584007913129639936))

(check-sat)
(get-info :reason-unknown)

(pop)
(push)

; but we also know instantly that its condition, ((I * (I + 1)) mod 2 = 0) \/ (I * (I + 1) >= 0), is unsat
(assert (not (or (= 0 (mod (* I (+ I 1)) 2)) (>= (* I (+ I 1)) 0))))
(check-sat)

(pop)
(push)

; and instantly that the then branch is SAT
(assert (< (+ S (div (* I (+ I 1)) 2) ) 115792089237316195423570985008687907853269984665640564039457584007913129639936))
(check-sat)

(pop)
(push)

; and instantly that the else branch is SAT
(assert (< (+ S (ite (> 2 0) (+ (div (* I (+ I 1)) 2) 1) (- (div (* I (+ I 1)) 2) 1))) 115792089237316195423570985008687907853269984665640564039457584007913129639936))
(check-sat)

[HuStmpHrrr]

when I removed the first (push), it gives a sat quite instantly.

[PetarMax]

Understood, but that is not the use case that we have. This is part of a branching check, which we do by first checking that a ground truth (in this case, everything before the first (push) ) is SAT, then push, add the branching constraint, check SAT, pop, add its negation, and check SAT again. The script mirrors that use case. Perhaps a better example is

(set-option :timeout 1000)

(declare-const G Int)
(declare-const I Int)
(declare-const S Int)

(assert (<= 1 G))
(assert (<= 0 I))
(assert (<= 0 S))
(assert (<= (+ (* 52 I) 21) G))
(check-sat)

(push)

; This times out
(assert (< (+ S (ite (or (= 0 (mod (* I (+ I 1)) 2)) (>= (* I (+ I 1)) 0)) (div (* I (+ I 1)) 2) (ite (> 2 0) (+ (div (* I (+ I 1)) 2) 1) (- (div (* I (+ I 1)) 2) 1)))) 115792089237316195423570985008687907853269984665640564039457584007913129639936))
(check-sat)
(get-info :reason-unknown)

(pop)

; This also times out
(assert (not (< (+ S (ite (or (= 0 (mod (* I (+ I 1)) 2)) (>= (* I (+ I 1)) 0)) (div (* I (+ I 1)) 2) (ite (> 2 0) (+ (div (* I (+ I 1)) 2) 1) (- (div (* I (+ I 1)) 2) 1)))) 115792089237316195423570985008687907853269984665640564039457584007913129639936)))
(check-sat)
(get-info :reason-unknown)

We have not had issues with this with v4.13.0 or with earlier versions.

Separately, if you remove the first (push) then what does the subsequent (pop) pop? I would think that then the reasoning is not performed in the desired context, which is

(assert (<= 1 G))
(assert (<= 0 I))
(assert (<= 0 S))
(assert (<= (+ (* 52 I) 21) G))

Is that correct?

[HuStmpHrrr]

I am not a maintainer. I am just interested in this issue.

I am a bit surprised that you said that this does not occur in prior versions. In my quick test, I am seeing that it only returns sat in 4.11.0. All other versions, including 4.13.0 and 4.12.x, time out for me with a 5 sec limit.

[PetarMax]

I'm not sure why, but we definitely do not have this issue with v4.13.0. I also do not have this issue in v4.13.4 on my M1 Mac, but in our CI, which is on Linux, it does manifest.

There is an additional bit of complexity that I cannot explain either - we run the SAT checks with several retries and doubling the timeout, but the results are inconsistent. In particular, on Linux the check always returns unknown no matter the retries and initial timeout, but on my M1 Mac the check passes correctly if there is one retry, but not if there isn't even if I increase the timeout beyond the double, which is very unusual.

[NikolajBjorner]

It may happen that platform divergence is due to:

• different handling of timeouts/processor speed
• semantic differences based on C++ underspecified behavior (evaluation order of function arguments). Unexpected performance divergence on identical inputs between macOS and Linux #7457
• blatant code bugs. Z3 should behave the same across platforms modulo timeouts.

The default solver isn't great at pre-processing with incremental solving. If you use sat.smt=true it is more capable.

[jberthold]

I'm not sure why, but we definitely do not have this issue with v4.13.0. I also do not have this issue in v4.13.4 on my M1 Mac, but in our CI, which is on Linux, it does manifest.

Correction on this statement: @PetarMax uses a Mac and was maybe able to make the script pass on a second attempt somehow.
I have tested this on Linux (using our docker images that we maintain to provide z3), and the script also times out on 4.13.0, but sometimes reports a different reason (incomplete (theory arithmetic) instead of canceled).

On the plus side, the sat.smt=true option makes both versions solve this instantly.