Eldarica returns SAT for unsat file

[kensingRichardt]

Hi,

I think I found another bug with the latest version of eldarica:

(set-logic HORN)
(define-fun arrayEq ((ar1 (Array Int Int)) (ar2 (Array Int Int))) Bool (forall ((i Int)) (= (select ar1 i) (select ar2 i))))

(assert (forall (
         (j (Array Int Int))
         (o (Array Int Int))
        )
    (=> (and (arrayEq j o) (= 1 (select o 1)) (= j (store (store o 0 0) 0 0))) false)))

(check-sat)

Eldarica returns sat:

$ ~/eldarica/eld  test.smt2 
sat

However the correct answer should be UNSAT, as the LHS of the assertion is satisfied for an array [0,1,...].
Interestingly re-defining arrayEq as
(define-fun arrayEq ((ar1 (Array Int Int)) (ar2 (Array Int Int))) Bool (= ar1 ar2))
allows eldarica to find the formula UNSAT.

[kensingRichardt]

Have you had a chance to take a look at this?

[pruemmer]

I have looked into the problem, but not have time yet to do anything about this. The issue is that the input is really beyond the fragment supported by Eldarica; we cannot handle clauses with universally quantified constraints (over arrays) in a complete way. The correct behaviour would be to reject this input file.