Eldarica reports wrong answer

[kensingRichardt]

Hello everyone,

it seems that eldarica returns the wrong answer for the following code:

(set-logic HORN)

(declare-fun P_undef ((Array Int Int) (Array Int Int) Int) Bool)

(assert (forall (
         (Y1 Int)
         (U2 (Array Int Int))
         (V2 (Array Int Int))
        )
    (or 
      (P_undef V2 U2 Y1) 
      (and (>= (select U2 4) 3)  (= U2 (store U2 (+ Y1 (select V2 0)) 2)))
      (and (<= (select U2 4) 3)  (= U2 (store U2 (+ Y1 (select V2 0)) 2)))
      )))

(assert (forall ( (T1 (Array Int Int)))
    (not (P_undef T1 (store T1 (+ 4 (select T1 0)) 2) 4))))

(check-sat)

I invoked eldarica with ~/eldarica/eld -ssol -splitClauses:0 sat.smt2

A model is given by: (define-fun P_undef ((A (Array Int Int)) (B (Array Int Int)) (C Int)) Bool (and (or (<= (select B 4) 2) (not (= B (store B (+ C (select A 0)) 2)))) (or (>= (select B 4) 4) (not (= B (store B (+ C (select A 0)) 2)))))) and eldarica is even able to verify that.

[pruemmer]

That's another great catch, thanks for the bug report! The problem turned out to be a case of incorrect theory combination in the SMT solver Princess. After a rebuild (run sbt clean first), the answer should be correct now.

[kensingRichardt]

Great. Eldarica now returns SAT and a model instead of UNSAT.