Closed
Description
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?