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) Bool)
(declare-fun Q (Int) Bool)

(assert (forall ((x Int) (y Int))
  (=> (Q x) (P x y))))
  
(assert (forall ((x Int) (y Int)) (=> (>= y 1) (Q x))))

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

z3 returns

sat
(
  (define-fun Q ((x!0 Int)) Bool
    false)
  (define-fun P ((x!0 Int) (x!1 Int)) Bool
    true)
)

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

This problem is similar to #5863 which returned after the 2b6dadc.

[hgvk94]

None of your instances have a query clause. So the trivial model (all predicates True) should work on all of them. I can try to fix them but unfortunately, I am nowhere near as fast as @NikolajBjorner.

[NikolajBjorner]

The bugs are now mostly in dl_mk_rule_inliner (the first bug was in coi-filter, but that seems to be handled).
It can be isolated to the calls to datalog::del_rule
The second argument indicates how to update the model when a rule is deleted. This functionality was an afterthought and not properly debugged.
The behavior of del_rule prior to dealing with these bugs was to replace the interpretation of a removed rule to contribute with the interpretation "false". The correct interpretation is typically to include the constraints from the body, but I am fixing instances incrementally based on bug reports. If you go over the code you can code-review the different instances where rules are removed and determine what the correct model reconstruction would be. There are around 6 calls to datalog::del_rule each under a different case analysis. The code is a bit convoluted as well so reviewing it isn't necessarily easy. If there is a way to retain the effect of the simplification yet streamline the code it would be good.

[NikolajBjorner]

The way to debug it is to run with -tr:dl -v:10 and establish where the rules are removed and what the instruction to model reconstruction is. It then very directly points to the position in the code that makes the faulty reconstruction.