Wrong result "unsat" for Spacer

[jena-kling]

Hello guys,

I think I found another bug for Spacer where it erroneously returns unsat. This seems to be connected to inlining of rules :

(set-logic HORN)

(declare-fun inv1 (Int Int Int) Bool)
(declare-fun u_pred (Int) Bool)

(assert (u_pred 0))
(assert (inv1 0 0 8))
(assert (forall ((D (Array Int Int)) (F Int) (H Int))
  (=> (inv1 F 0 8) (inv1 (+ 1 F) H (select (store D F 0) H)))))
(assert (forall ((D Int)) (=> (and (inv1 1 D 8) (u_pred D)) false)))

(check-sat)

Specifically I executed:

$ z3 fp.xform.inline_eager=false test.smt2 
unsat

$ z3 --version
Z3 version 4.13.4 - 64 bit - build hashcode 943d881340fc77496dcfc75d9ba65a617a51475e

[NikolajBjorner]

Looks like blame is EMBP for Arrays:

-------- [spacer] spacer::pred_transformer::mk_rf C:\z3\src\muz\spacer\spacer_context.cpp:3970 ---------
Reach fact, before QE:
(and (= inv1_2_0 8)
     (= inv1_0_n (+ 1 inv1_0_0))
     (= inv1_0_0 0)
     (= inv1_1_0 0)
     (= inv1_2_n (select (store aux!1_n inv1_0_0 0) inv1_1_n)))
Vars:

inv1_0_0
inv1_1_0
inv1_2_0
aux!1_n
------------------------------------------------
-------- [spacer] spacer::pred_transformer::mk_rf C:\z3\src\muz\spacer\spacer_context.cpp:3984 ---------
Reach fact, after QE project:
(= inv1_0_n 1)
Vars:

------------------------------------------------

Let us call the state variables x, y, z, x', y', z', with array A.

Then it says x = y = 0, z = 8, x' = x + 1, z' = A[x -> 0][y']
Project everything but x', y', z'.
If x = y' then z' = 0. So, the projection must have either x' -1 != y' or z' = 0
The projection has x' = 1 as expected from x' = x + 1.

Tracing with qe, it narrows to mbp_tg:

-------- [qe] qe::mbproj::impl::spacer_qel C:\z3\src\qe\qe_mbp.cpp:555 ---------
Before projection:
(and (= inv1_2_0 8)
     (= inv1_0_n (+ 1 inv1_0_0))
     (= inv1_0_0 0)
     (= inv1_1_0 0)
     (= inv1_2_n (select (store aux!1_n inv1_0_0 0) inv1_1_n)))
Vars: 
inv1_0_0
inv1_1_0
inv1_2_0
aux!1_n
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_2_0 := 8
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_2_0 := 8
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_0_0 := (+ inv1_0_n (* (- 1) 1))
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_0_0 := (+ (* (- 1) 1) inv1_0_n)
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_1_0 := 0
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_1_0 := 0
------------------------------------------------
-------- [qe] qe::mbproj::impl::do_qel C:\z3\src\qe\qe_mbp.cpp:532 ---------
After qel:
(and (= 1 inv1_0_n) (= inv1_2_n (select (store aux!1_n 0 0) inv1_1_n)))
Vars: 
aux!1_n
------------------------------------------------
-------- [qe] qe::mbproj::impl::qel_project C:\z3\src\qe\qe_mbp.cpp:551 ---------
After mbp_tg:
(= inv1_0_n 1) models 1
Vars: 
------------------------------------------------
-------- [spacer] spacer::pred_transformer::mk_rf C:\z3\src\muz\spacer\spacer_context.cpp:3984 ---------
Reach fact, after QE project:
(= inv1_0_n 1)
Vars:

[NikolajBjorner]

@hgvk94

[NikolajBjorner]

m_use_mdl is false when mbp_arrays_tg is invoked.
Then the rule for eliminating read-writes is not invoked.

z3/src/qe/mbp/mbp_arrays_tg.cpp

Line 364 in 42f6e13

if (m_use_mdl && is_rd_wr(nt)) {

If you force m_use_mdl = true, we get the right results.