Invalid model is generated but not reported with option model-validate

[kensingRichardt]

Hi,

I am working with Z3/Spacer (Z3 version 4.13.0 - 64 bit) and found an issue with the following code:

(set-logic HORN)

(declare-fun pred (Int Int) Bool)
(assert (not (pred 1 1)))
(assert (pred 8 8))
(assert (forall ((N Int)) (=> (pred 1 9) (pred 1 N))))
(assert (forall ((Unused Int)) (=> (pred 2 2) false)))

(check-sat)

If I call z3 -model model-validate=true test.smt2 I get

sat
(
  (define-fun pred ((x!0 Int) (x!1 Int)) Bool
    (and (not (>= x!1 9)) (not (<= x!1 1))))
)

The model is invalid (contradicting the last assertion) and z3 misses to report a warning about this.

[NikolajBjorner]

it is a known issue that you have to turn off pre-processing to ensure correct models. Pre-processing discovers that pred(2,2) doesn't resolve and therefore the clause can be removed. The relevant steps for adjusting the model of the remaining clauses are not taken. We have punted on this given that model correctness can be ensured by disabling fp.xform preprocessing options.