z3/spacer returning UNSAT for sat-instance

[jena-kling]

Hey everyone,

for this case z3 returns unexpectedly UNSAT:

(set-logic HORN)

(declare-datatypes ((arr_int_tuple 0)) (((arr_int_tuple (d (Array Int Int)) (e Int)))))
(declare-datatypes ((dtp 0)) (((dtp (g (Array Int arr_int_tuple)) (h Int)))))

(declare-fun p (Int (Array Int dtp) (Array Int dtp)) Bool)
(declare-fun bin_p_arr ((Array Int dtp) (Array Int dtp)) Bool)
(declare-fun p_arr ((Array Int dtp)) Bool)

(assert (forall ((aj (Array Int dtp))) (p 1 aj aj)))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp))) (=> (bin_p_arr aj aj) (bin_p_arr aj ak))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)))
  (=>  (p_arr aj) (not (p 3 aj ak)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)) (ap dtp))
  (or (p (h ap) aj ak) (not (bin_p_arr aj ak)) (not (= (h ap) 0)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)))
  (or (p_arr ak) (not (bin_p_arr aj aj)) (not (p 0 aj ak)))))
(assert (forall ((aj (Array Int dtp)))
  (let ((a!1 (e (select (g (select aj 0)) 0))))
    (or (p_arr aj) (<= a!1 0)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)))
  (let ((a!1 (e (select (g (select ak 0)) 0))))
    (or (not (p 0 aj ak)) (not (<= a!1 0)) (p 3 aj aj)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)) (o (Array Int dtp)) (r arr_int_tuple))
  (let ((a!1 (e (select (g (select ak 0)) 0)))
        (a!2 (e (select (g (select aj 0)) 0)))
        (a!3 (store (g (select ak 0)) 1 (arr_int_tuple (store (d r) 0 0) 0))))
    (or (<= (+ a!1 (* (- 1) a!2)) 0) (bin_p_arr aj (store o 0 (dtp a!3 0)))))))

(check-sat)

A model is given by:

(define-fun bin_p_arr ((x!0 (Array Int dtp)) (x!1 (Array Int dtp))) Bool
    (let ((a!1 (e (select (g (select x!0 0)) 0)))
          (a!2 (e (select (g (select x!1 0)) 0))))
      (not (>= (+ a!1 (* (- 1) a!2)) 0))))
(define-fun p ((x!0 Int) (x!1 (Array Int dtp)) (x!2 (Array Int dtp))) Bool
  (let ((a!1 (e (select (g (select x!1 0)) 0)))
        (a!2 (e (select (g (select x!2 0)) 0))))
  (let ((a!3 (not (>= (+ a!1 (* (- 1) a!2)) 0))))
    (and (or (not (>= x!0 3)) (not (>= a!1 0))) (or (not (<= x!0 0)) a!3)))))
(define-fun p_arr ((A (Array Int dtp))) Bool (>= (e (select (g (select A 0)) 0)) 1))

Contrary to #7466 , this seems to be independent from slicing as we also have

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

I am using Z3 version 4.13.0 - 64 bit.
Is this also a bug?

[hgvk94]

Initially, I suspected it to be a bug in the new mbp. But that doesn't seem to be the case. Looking into it....

[hgvk94]

This problem exposes 2 bugs: one in the previous MBP and one in QEL. In the previous MBP, variable are not removed. In QEL, one of the axioms is not applied properly (the rule to factor out read terms as new variables)

To reproduce the QEL issue:
(declare-datatypes ((arr_int_tuple 0)) (((arr_int_tuple (d (Array Int Int)) (e Int))))) (declare-datatypes ((dtp 0)) (((dtp (g (Array Int arr_int_tuple)) (h Int))))) (declare-fun a () (dtp)) (declare-fun b () (dtp)) (assert (and (<= (e (select (g a) 0)) 0) (not (<= (e (select (g a) 0)) (e (select (g b) 0)))))) (check-sat) (mbp (and (<= (e (select (g a) 0)) 0) (not (<= (e (select (g a) 0)) (e (select (g b) 0))))) (a))
returns true where it should have returned (<= (e (select (g b) 0)) (-1))