Fix bugs in `QF_ALIA`

[Tomaqa]

There are wrong answers to several incremental queries in benchmark incremental/QF_ALIA/UltimateBuchiAutomizer/LexIndexValue-Pointer_true-termination.c.smt2 (sat instead of unsat).

[blishko]

Here is a minimal example of the incorrect answer.

(set-logic QF_ALIA)
(declare-fun v () Int)
(declare-fun a () (Array Int Int))
(assert (= a (store a v 0)))
(push 1)
(assert (= 0 v))
(push 1)
(assert false)
(check-sat)
(pop 1)
(assert (> 0 (select a 0)))
(check-sat)

OpenSMT responds

unsat
sat

but it should be

unsat
unsat

[Tomaqa]

Unfortunately, within incremental/QF_ALIA/UltimateBuchiAutomizer, #711 fixed benchmark LexIndexValue-Pointer_true-termination.c.smt2 (although still only 10 minutes of computation is analyzed then it timeouts), but wrong answers remain for other benchmarks such as CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i.smt2 and CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i.smt2 which finishes within 10 minutes.

[Tomaqa]

Unfortunately, these benchmarks fail also with release 2.5.2, so this bug originates from an earlier code.

[blishko]

This seems to be a bug in the core of the array solver (or something missing in the preprocessing). The bug does not need incrementality, nor arithmetic.

Here are two examples, one for QF_ALIA, one for QF_AX (single-query), for which OpenSMT answers sat, but they are unsat.

(set-logic QF_ALIA)
(declare-fun a () (Array Int (Array Int Int)))
(declare-fun b () (Array Int Int))
(assert (not (= b (select a 1))))
(assert (= a (store (store a 1 b) 0 b)))
(check-sat)

(set-logic QF_AX)
(declare-sort E 0)
(declare-fun a () (Array E (Array E E)))
(declare-fun b () (Array E E))
(declare-fun e () E)
(declare-fun f () E)
(assert (distinct e f))
(assert (not (= b (select a e))))
(assert (= a (store (store a e b) f b)))
(check-sat)

[Tomaqa]

PR #717 resolves CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i.smt2 and java_Sequence-alloca_true-termination.c.i.smt2 in incremental/QF_ALIA/UltimateBuchiAutomizer, but does not resolve CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i.smt2 where the very last query still fails.

[blishko]

Here is a minimized example for the last wrong answer. It is a bit more complicated than before. I still need to investigate.

(set-logic QF_ALIA)
(push 1)
(declare-fun n () Int)
(declare-fun m () Int)
(declare-fun a () (Array Int (Array Int Int)))
(assert (= 0 (select (select a m) 0)))
(assert (= a (store a 0 (select (store a n (select a 0)) m))))
(check-sat)
(pop 1)
(declare-fun n () Int)
(declare-fun m () Int)
(declare-fun a () (Array Int (Array Int Int)))
(declare-fun b () (Array Int Int))
(assert (not (= n m)))
(assert (not (= 0 (select (select a n) 0))))
(assert (= (select b 0) 0))
(assert (= a (store (store a n b) m (select a 0))))
(check-sat)

Looks like it might be related to name clashes in OpenSMT, because if I rename the second declaration of m to x, OpenSMT answers correctly.

[blishko]

Here is another, simple example.

(set-logic QF_ALIA)
(declare-fun n () Int)
(declare-fun m () Int)
(declare-fun x () Int)
(declare-fun a () (Array Int Int))
(push 1)
(assert (= 0 (select a m)))
(assert (= a (store a 0 (select (store a n 0) m))))
(check-sat)
(pop 1)
(assert (not (= n m)))
(assert (= m (select a x)))
(assert (= n (select a x)))
(check-sat)

[Tomaqa]

I confirm that both the two examples above fail (i.e. answer 2x sat instead of sat and unsat) not only with the current version but also with version 2.5.2.

[blishko]

Finally resolved by #718.