CODEWITHSUNDEEP
z3
Guilhem Jaber
Guilhem Jaber

Reputation: 33

Satisfiability of Presburger Formulas with z3

I'm using z3 (v4.3.2 32bit on Linux) to decide satisfiability of Presburger Arithmetic formulas, but I have a problem with the following formula : 

(assert (forall ((x1 Int) (x2 Int) (x3 Int))
                  (=> (and (= x3 1) (= x1 (- x2))) 
                      (forall ((x4 Int) (x5 Int) (x6 Int)) 
                              (=> (= x6 x2) 
                                  (exists ((y Int)) 
                                          (=> (= x5 (+ x6 (- x4))) 
                                              (and (= (+ x1 x4) y) 
                                                   (= x5 (- y)) 
                                                   (= (+ x1 x4) (- x5))
                                              )
                                          )
                                  )
                              )
                      )
                  )
        )
)

(check-sat)

I'm quite sure that this formula is satisfiable, but z3 answers "unsat". In fact, if I try to change a bit the formula, z3 answers "sat", like with the following formula 

(assert (forall ((x3 Int) (x1 Int) (x2 Int))
                  (=> (and (= x3 1) (= x1 (- x2))) 
                      (forall ((x4 Int) (x5 Int) (x6 Int)) 
                              (=> (= x6 x2) 
                                  (exists ((y Int)) 
                                          (=> (= x5 (+ x6 (- x4))) 
                                              (and (= (+ x1 x4) y) 
                                                   (= x5 (- y)) 
                                                   (= (+ x1 x4) (- x5))
                                              )
                                          )
                                  )
                              )
                      )
                  )
        )
)

(check-sat)

where I've just switched the quantification on x3 in top of the list of the first forall quantification. If I also remove the x3 variable, which is in fact useless, z3 also answers "sat". Is there something I don't understand or is this a bug ?

Upvotes: 3

Views: 326

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Thanks for pointing this out. This is a bug in the quantifier elimination modules that affects cases of nested quantifiers. It is now fixed in the unstable branch.

Upvotes: 2

Related Questions