Z3 returns incorrect 'unsat' in QF_NRA logic

[aleksanderJunge]

Hi Z3 team,

I encountered a peculiar issue with Z3 incorrectly returning unsat, for a formula in the 'QF_NRA' logic. Funny enough, if I add an additional constraint, Z3 will realize that it is indeed sat. This problem occurs with version 4.13.0 of Z3, I tried an older version (4.8.6), which doesn't seem to suffer from this problem.

In more detail:
We have some Real variables:

( declare-const a_t0_3   Real)
( declare-const a_t1_3   Real)
( declare-const a_t2_3   Real)

that once each is assigned 8 should give sat. And indeed asserting:

...
(assert (= a_t0_3 8))
(assert (= a_t1_3 8))
(assert (= a_t2_3 8))
(assert (= (+ a_t0_3 a_t1_3 a_t2_3) 24))
...

returns sat. HOWEVER, removing all 3 assertions and just leaving the last line:

...
(assert (= (+ a_t0_3 a_t1_3 a_t2_3) 24))
...

makes the formula unsatisfiable. Leaving any of the 3 assertions on the individual variables is also sufficient to make z3 realize it is sat.

The full .smt2 file can be seen below:

(set-logic QF_NRA)

( declare-const a_t0_0   Real)
( declare-const a_t1_0   Real)
( declare-const a_t2_0   Real)
( declare-const l_t0t1_0 Real)
( declare-const r_t0t1_0 Real)
( declare-const l_t1t2_0 Real)
( declare-const r_t1t2_0 Real)
( declare-const l_t2t0_0 Real)
( declare-const r_t2t0_0 Real)

( declare-const a_t0_1   Real)
( declare-const a_t1_1   Real)
( declare-const a_t2_1   Real)
( declare-const l_t2t0_1 Real)
( declare-const r_t2t0_1 Real)
( declare-const l_t1t2_1 Real)
( declare-const r_t1t2_1 Real)
( declare-const l_t0t1_1 Real)
( declare-const r_t0t1_1 Real)
( declare-const from_1   Real)
( declare-const   to_1   Real)
( declare-const payout_1 Real)

( declare-const a_t0_2   Real)
( declare-const a_t1_2   Real)
( declare-const a_t2_2   Real)
( declare-const l_t2t0_2 Real)
( declare-const r_t2t0_2 Real)
( declare-const l_t1t2_2 Real)
( declare-const r_t1t2_2 Real)
( declare-const l_t0t1_2 Real)
( declare-const r_t0t1_2 Real)
( declare-const from_2   Real)
( declare-const   to_2   Real)
( declare-const payout_2 Real)

( declare-const a_t0_3   Real)
( declare-const a_t1_3   Real)
( declare-const a_t2_3   Real)
( declare-const l_t2t0_3 Real)
( declare-const r_t2t0_3 Real)
( declare-const l_t1t2_3 Real)
( declare-const r_t1t2_3 Real)
( declare-const l_t0t1_3 Real)
( declare-const r_t0t1_3 Real)
( declare-const from_3   Real)
( declare-const   to_3   Real)
( declare-const payout_3 Real)

; user assertions
(assert ( = a_t0_0 (/ 6 1)))
(assert ( = a_t1_0 (/ 6 1)))
(assert ( = a_t2_0 (/ 6 1)))
(assert (>= a_t0_1 0))
(assert (>= a_t1_1 0))
(assert (>= a_t2_1 0))
(assert (>= a_t0_2 0))
(assert (>= a_t1_2 0))
(assert (>= a_t2_2 0))
(assert (>= a_t0_3 0))
(assert (>= a_t1_3 0))
(assert (>= a_t2_3 0))

; HERE ARE THE VARIABLES OF INTEREST:
;(assert (= a_t0_3 8))
;(assert (= a_t1_3 8))
;(assert (= a_t2_3 8))
(assert (= (+ a_t0_3 a_t1_3 a_t2_3) 24))

; amm assertions
(assert (= (/ 18 1) l_t0t1_0))
(assert (= (/ 8 1)  r_t0t1_0))
(assert (= (/ 18 1) l_t1t2_0))
(assert (= (/ 8 1)  r_t1t2_0))
(assert (= (/ 18 1) l_t2t0_0))
(assert (= (/ 8 1)  r_t2t0_0))

;txn assertions
(assert (> from_1 0))
(assert (> from_2 0))
(assert (> from_3 0))
(assert (> to_1 0))
(assert (> to_2 0))
(assert (> to_3 0))

(assert (= 
            payout_1
            (/ 
               (* from_1 l_t1t2_0)
               (+ from_1 r_t1t2_0))
        )
)
(assert (ite 
    (and (>= to_1 0) (<= to_1 payout_1))
    (and 
        (= l_t1t2_1 (- l_t1t2_0 payout_1))
        (= r_t1t2_1 (+ r_t1t2_0 from_1))
        (= a_t1_1 (+ a_t1_0 payout_1))
        (= a_t2_1 (- a_t2_0 from_1))
    )
    (and
        (= l_t1t2_1 l_t1t2_0 )
        (= r_t1t2_1 r_t1t2_0 )
        (= a_t1_1 a_t1_0 )
        (= a_t2_1 a_t2_0 )
    )
))

(assert (= 
            payout_2
            (/ 
               (* from_2 l_t2t0_1)
               (+ from_2 r_t2t0_1))
        )
)
(assert (ite 
    (and (>= to_2 0) (<= to_2 payout_2))
    (and 
        (= l_t2t0_2 (- l_t2t0_1 payout_2))
        (= r_t2t0_2 (+ r_t2t0_1 from_2))
        (= a_t0_2 (- a_t0_1 from_2))
        (= a_t2_2 (+ a_t2_1 payout_2))
    )
    (and
        (= l_t2t0_2 l_t2t0_1 )
        (= r_t2t0_2 r_t2t0_1 )
        (= a_t0_2 a_t0_1 )
        (= a_t2_2 a_t2_1 )
    )
))

(assert (= 
            payout_3
            (/ 
               (* from_3 l_t0t1_2)
               (+ from_3 r_t0t1_2))
        )
)
(assert (ite 
    (and (>= to_3 0) (<= to_3 payout_3))
    (and 
        (= l_t0t1_3 (- l_t0t1_2 payout_3))
        (= r_t0t1_3 (+ r_t0t1_2 from_3))
        (= a_t0_3 (+ a_t0_2 payout_3))
        (= a_t1_3 (- a_t1_2 from_3))
    )
    (and
        (= l_t0t1_3 l_t0t1_2 )
        (= r_t0t1_3 r_t0t1_2 )
        (= a_t1_3 a_t1_2 )
        (= a_t0_3 a_t0_2 )
    )
))

; unchanged amms
(assert (= l_t2t0_1 l_t2t0_0))
(assert (= r_t2t0_1 r_t2t0_0))
(assert (= l_t0t1_1 l_t0t1_0))
(assert (= r_t0t1_1 r_t0t1_0))

(assert (= l_t1t2_2 l_t1t2_1))
(assert (= r_t1t2_2 r_t1t2_1))
(assert (= l_t0t1_2 l_t0t1_1))
(assert (= r_t0t1_2 r_t0t1_1))

(assert (= l_t2t0_3 l_t2t0_2))
(assert (= r_t2t0_3 r_t2t0_2))
(assert (= l_t1t2_3 l_t1t2_2))
(assert (= r_t1t2_3 r_t1t2_2))

; unchanged user wals
(assert (= a_t0_1 a_t0_0))
(assert (= a_t1_2 a_t1_1))
(assert (= a_t2_3 a_t2_2))

(check-sat)

I tried to introduce named assertions and use the (get-unsat-core) feature to investigate this a bit further, however then z3 doesn't terminate (at least not after 20 minutes, where it previously took 2 seconds without the (get-unsat-core)).

Attached is also the zipped version of the (get-unsat-core) file.

Hope you can help figure out what is going wrong here.

Cheers, Aleksander

files.zip