Disabling fp.xform.inline_eager results in an incorrect model

[AnzhelaSukhanova]

Hello,
For this instance

(set-logic HORN)

(set-option :fp.xform.inline_eager false)

(declare-fun P (Int  Int  Int) Bool)
(declare-fun Q (Int  Int  Int  Int) Bool)

(assert (forall ((a Int) (b Int) (c Int) (d Int))
  (=> (and (Q a b c d)
           (<= (+ 1 d) a)
           (<= (+ 1 c) b))
      (P a b c))))

(assert (forall ((a Int) (b Int) (c Int) (d Int))
  (=> (>= a 1) (Q a b c d))))

(check-sat)
(get-model)
(exit)

z3 returns

sat
(
  (define-fun P ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
    (exists ((x!3 Int))
      (! (and (<= x!3 (+ (- 1) x!0)) (<= x!2 (+ (- 1) x!1)) (>= x!0 1))
         :weight 0)))
  (define-fun Q ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
    false)
)

For a >= 1 in second clause this interpretation is incorrect.
With fp.xform.inline_eager it returns correct model.

[AnzhelaSukhanova]

@NikolajBjorner, this problem came back after the last commit.