Z3 diverges on example from Bradley's IC3 paper

[Columpio]

For the following problem taken from Bradley "Understanding IC3" paper the recent release of Z3 diverges:

(set-logic HORN)

(declare-fun I (Int Int) Bool)
(assert (forall ((x Int) (y Int)) (=> (and (= x 1) (= y 1)) (I x y))))
(assert (forall ((x Int) (y Int) (x1 Int) (y1 Int)) (=> (and (= x1 (+ x 1)) (= y1 (+ y x)) (I x y)) (I x1 y1))))
(assert (forall ((x Int) (y Int)) (=> (I x y) (>= y 1))))

(check-sat)
(get-model)

Run on Z3 version 4.8.17 - 64 bit on Ubuntu 20.04 both with z3 file.smt2 and z3 fp.engine=spacer file.smt2.
Note that this example still works on Z3 4.7.1, immediately giving:

sat
(model (define-fun I ((x!0 Int) (x!1 Int)) Bool (and (>= x!1 1) (>= x!0 1))))

But it already does not work on Z3 4.8.1.

Interestingly, if we apply a global guidance from #6026 with fp.spacer.global=true, this example works again.

[agurfinkel]

interpolation is inherently unstable. different interpolants give different results. Global guidance is an attempt to address this issue. I'm currently working on merging Spacer Global Guidance into master. I will keep this issue open until GG is merged.

[NikolajBjorner]

GG was merged.

[Columpio]

@agurfinkel for some reason it does not work now even with global guidance.
That is, I run:

$ z3 --version
Z3 version 4.12.2 - 64 bit - build hashcode c2fe76569fdb118101e8131f982cc5bfd7cc4438
$ z3 bradley.smt2
<diverges>
$ z3 fp.spacer.global=true bradley.smt2
<diverges>

So, @NikolajBjorner, I do not think this issue can be closed right now.

[hgvk94]

The instance is solved right now. Can we close this issue?