z3 returning wrong sat-answer

[jena-kling]

Hello everyone,

I am currently working with Z3 version 4.13.0 and think that z3 returns erroneously SAT for the following CHC-formula:

(set-logic HORN)

(declare-fun inv1 (Int (Array Int Int) Int Int Int) Bool)
(declare-fun inv2 ((Array Int Int) (Array Int Int) Int Int Int) Bool)

(assert (inv1 1 (store  ((as const (Array Int Int)) 0)  1 (- 1)) 0 0 2))
(assert (forall ((A (Array Int Int))
         (B Int)
         (C Int)
         (D Int)
         (E Int)
         (F Int)
         (myunused Int))
  (let ((a!1 (= E (ite (<= C (select A B)) C (select A B)))))
    (=> (and (inv1 myunused A B C D) (= F (+ 1 B)) (> D B) a!1)
        (inv1 2 A (+ 1 B) E D)))))
(assert (forall ((A (Array Int Int))
         (B Int)
         (C Int)
         (D Int)
         (E (Array Int Int))
         (myunused Int))
  (=> (and (inv1 myunused A B C D) (>= B D) ) (inv2 A E C 0 D))))
(assert (forall ((A (Array Int Int))
         (B (Array Int Int))
         (C Int)
         (F (Array Int Int)))
  (let ((a!1 (and (inv2  A B C 0 2)
                  (= (store B 1 (select A 1)) F))))
    (=> a!1 (inv2 A F (+ 1 C) 0 2)))))
(assert (forall ((A (Array Int Int))
         (B (Array Int Int))
         (C Int)
         (D Int)
         (E Int)
         (F Int))
  (let ((a!1 (and (inv2 A B C D E)
                  (>= C F)
                  (> E F)
                  (> F 0)
                  )))
    (=> a!1 false))))
    
(check-sat)

I get

$ z3 unsat.smt2 
sat

However it seems that the formula is UNSAT and eldarica can even give an unsat proof:

$ ~/eldarica/eld -assert -scex unsat.smt2 
unsat

0: false -> 1
1: (inv2 (store ((as const (Array Int Int)) 0) 1 (- 1)) (store ((as const (Array Int Int)) 2) 1 (- 1)) 1 0 2) -> 2
2: (inv2 (store ((as const (Array Int Int)) 0) 1 (- 1)) (store ((as const (Array Int Int)) 2) 1 (- 1)) 0 0 2) -> 3
3: (inv2 (store ((as const (Array Int Int)) 0) 1 (- 1)) ((as const (Array Int Int)) 2) (- 1) 0 2) -> 4
4: (inv1 2 (store ((as const (Array Int Int)) 0) 1 (- 1)) 2 (- 1) 2) -> 5
5: (inv1 2 (store ((as const (Array Int Int)) 0) 1 (- 1)) 1 0 2) -> 6
6: (inv1 1 (store ((as const (Array Int Int)) 0) 1 (- 1)) 0 0 2)

I already minimized the SMT-file. Thanks in advance.

[NikolajBjorner]

Note, debug mode produces:

(+ 2 (* (- 1) inv1_2_0))
coeff,lit,sum -1
(<= inv1_4_n 2)
(+ (* (- 1) inv1_2_0) inv1_4_n)
coeff,lit,sum 1
(not (<= (+ inv1_4_n (* (- 1) inv1_2_0)) 0))
1
coeff,lit,sum 2
(let ((a!1 (+ inv1_2_0 (* (- 1) (+ inv1_2_n (* (- 1) inv1_2_0))))))
  (not (>= a!1 0)))
(+ 2 (* 4 inv1_2_0) (* (- 2) inv1_2_n))
coeff,lit,sum 2
(<= (+ inv1_2_n (* (- 1) inv1_2_0)) 1)
(* 2 inv1_2_0)
coeff,lit,sum -1
(>= inv1_4_n 2)
(+ 2 (* 2 inv1_2_0) (* (- 1) inv1_4_n))
coeff,lit,sum -1
(>= (+ inv1_2_n (* (- 1) inv1_4_n)) 0)
(+ 2 (* 2 inv1_2_0) (* (- 1) inv1_2_n))
Arithmetic proof check failed: (<= (+ (* 2 inv1_2_0) (* (- 1) inv1_2_n)) (- 2))
Proof check failed
#832 := (* -1 inv1_4_n)
#833 := (+ inv1_2_n #832)
#834 := (>= #833 0)
#1456 := [hypothesis]: #834
#1011 := (>= inv1_4_n 2)
#1455 := [hypothesis]: #1011
#843 := (* -1 inv1_2_0)
#844 := (+ inv1_2_n #843)
#982 := (<= #844 1)
#5159 := [hypothesis]: #982
#3065 := (* -1 #844)
#3066 := (+ inv1_2_0 #3065)
#3062 := (>= #3066 0)
#5033 := (not #3062)
#5195 := [hypothesis]: #5033
[th-lemma arith farkas 2 2 -1 -1 #5195 #5159 #1455 #1456]: false
ASSERTION VIOLATION
File: C:\z3\src\muz\spacer\spacer_proof_utils.cpp
Line: 358
Failed to verify: pc.check(pf, side)