Spacer: New bug after previous fix?

[jena-kling]

Hello

thanks a lot for fixing my previous bug reports. I think one fix however introduced a new issue:
For the following CHC-instance z3 returns erroneously sat:

(set-logic HORN)
(declare-datatypes ((item 0)) (((item (data Int)))))
(declare-datatypes ((HeapObject 0)) (((O_item (getitem item)) (defObj))))
(declare-datatypes ((Heap 0)) (((HeapCtor  (HeapContents (Array Int HeapObject))))))

(declare-fun atom1 () Bool)
(declare-fun atom2 () Bool)
(declare-fun atom3 () Bool)
(declare-fun inv_main21873min (Heap) Bool)
(declare-fun u (Int) Bool)

(assert (u 1))
(assert (=> atom3 atom1))
(assert (=> atom3 (u 9)))
(assert (forall ((h Heap)) (=> (and atom1 (inv_main21873min h)) false)))
(assert (forall ((h Heap) (hh Heap) (idx Int) (p Heap))
  (let 
    ((a!2 
      (ite 
        (> idx 0)
        (select (HeapContents p) 1)
        defObj)))
    (=> 
      (and 
        (= h (ite  (> idx 0) (HeapCtor (store (HeapContents hh) idx defObj)) hh))
        ((_ is O_item) a!2)
        (= hh (ite  (> (data (getitem a!2)) 0) (HeapCtor (store (HeapContents p) (data (getitem a!2)) defObj)) p))) 
      (inv_main21873min h)))))

(assert (forall ((h Heap) (b Bool) (hh Heap))
    (=> 
      (and 
        (inv_main21873min hh)
        (= h (ite b (HeapCtor (store (HeapContents hh) 1 defObj)) hh))
        ((_ is O_item) (ite  b (select (HeapContents hh) 1) defObj)))  
      (inv_main21873min h))))
(assert (=> atom2 atom3))
(assert (forall ((arr (Array Int HeapObject)))
  (=> 
    ( and atom2 (= defObj (select arr 0))) 
    atom3)))
(assert (forall ((i Int)) (=> (u i) atom2)))

(check-sat) 

When using the latest version of z3 I get

$ ~/z3/build/z3 test.smt2 
sat

However this instance is unsat and before commit f50f211 (fixing #7505) z3 was able to give the correct answer:

$ ~/z3-bd3d288a085b1543e8130983be7e1bc1d1becb9f/build/z3 test.smt2
unsat

[NikolajBjorner]

@hgvk94 - this asserts if you run it with

• z3 7566.smt2 /v:2 /tr:mbp /tr:spacer /tr:qe

ASSERTION VIOLATION
File: C:\z3\src\qe\qe_mbp.cpp
Line: 607
!eval.is_false(fml)

---

-------- [qe] qe::mbproj::impl::qel_project C:\z3\src\qe\qe_mbp.cpp:551 ---------
After mbp_tg:
false models 0
Vars: