Invalid model bug?

[kensingRichardt]

Hello everyone,

it seems that eldarica returns an invalid model for the following code:

(declare-fun pl24 ( ( Array Int ( Array Int Int ) ) Bool ) Bool)
(declare-fun pbool ( Bool ) Bool)

(assert ( pbool false ))
(assert (forall ( ( m ( Array Int ( Array Int Int ) ) ) ) ( => ( pl24 m true ) false )))
(assert (forall ( ( m ( Array Int ( Array Int Int ) ) ) ( aq Bool ) ( ar1 ( Array Int ( Array Int Int ) ) ) ( ar2 ( Array Int Int ) ) ) ( => ( and ( pbool aq ) ( = m ( store ar1 1 ( store ar2 ( + ( ite ( <= ( mod ( + 5 ( mod 5 6 ) ) 6 ) 7 ) ( mod ( + ( mod 5 6 ) ) 6 ) 2 ) ) 0 ) ) ) ) ( pl24 m aq ) )))
(check-sat)

If I call ~/eldarica/eld -ssol test.smt2 I get

sat
(
    (define-fun pbool ((A Bool)) Bool (not (= A true)))
    (define-fun pl24 ((A (Array Int (Array Int Int))) (B Bool)) Bool (and (or (exists ((var0 Int)) (exists ((var1 Int)) (and (and (exists ((var2 Int)) (and (and (<= (* 6 var2) 5) (>= (* 6 var2) 0)) (and (and (>= (+ (* (- 6) var2) (* (- 6) var1)) (- 10)) (>= (+ (* 6 var2) (* 6 var1)) 5)) (>= (+ (* 6 var2) (* 6 var1)) 3)))) (and (and (<= (* 6 var1) 5) (>= (* 6 var1) 0)) (and (>= (+ (* (- 6) var1) (* (- 6) var0)) (- 5)) (>= (* 6 var1) (* (- 6) var0))))) (= (select (select A 1) (+ 5 (+ (* (- 6) var1) (* (- 6) var0)))) 0)))) (exists ((var0 (Array Int Int))) (exists ((var1 Int)) (exists ((var2 Int)) (exists ((var3 Int)) (exists ((var4 (Array Int (Array Int Int)))) (exists ((var5 Int)) (and (and (and (and (<= (* 6 var3) 5) (>= (* 6 var3) 0)) (and (and (>= (+ (* (- 6) var3) (* (- 6) var2)) (- 10)) (>= (+ (* 6 var3) (* 6 var2)) 5)) (>= (+ (* (- 6) var3) (* (- 6) var2)) (- 2)))) (= A (store (store var4 1 var0) 1 (store (store (select var4 1) var5 var1) 2 0)))) (= (select (select var4 1) var5) 0))))))))) (not (= B true))))
)

However replacing the declaration of pl24 with the given definition gives an UNSAT formula.

[pruemmer]

This bug took a bit of time to locate and fix. The problem was in the formula simplifier (in the SMT solver Princess), which turned a correct model into an incorrect one. The bug must have been in the solver since around 2010, so this is an awesome catch ;-)

[pruemmer]

Github was a bit too clever here and incorrectly closed this issue ...

[pruemmer]

But it should be fixed!