Invalid model for LIA instance

[rainoftime]

Hi,
For the following formula

(set-logic LIA)
(set-option :model_validate true)
(set-option :parallel.enable true)
(declare-const v6 Bool)
(declare-const v2 Bool)
(declare-const v7 Bool)
(declare-const i2 Int)
(declare-const i3 Int)
(push 1)
(assert (exists ((q4 Bool) (q5 Int) (q6 Bool) (q7 Bool)) (=> (or (distinct 50 67) q4 q7 q7 q7) (> q5 q5))))
(pop 1)
(assert (or v6 (distinct v7 (> i3 i2) v2) (> i3 i2)))
(check-sat-using (then simplify psat))

z3 Commit: 65b2037 gives a invalid model

failed to verify: (or v6 (not (<= i3 i2)))
evaluated to false
(params override_incremental true keep_cardinality_constraints true pb.solver solver xor_solver false inprocess.max 2 restart.max 5000 lookahead_simplify true retain_blocked_clauses false max_conflicts 4294967295)
v6 |-> 0
(<= i3 i2) |-> 1
sat
(error "line 13 column 37: an invalid model was generated")

[zhendongsu]

See #3552

[rainoftime]

@NikolajBjorner Maybe you can close this issue
and also
#3651
#3653

[rainoftime]

Similar issue #3628

[rainoftime]

@zhendongsu Hi, just an FYI. According to #3640, qffd tactic also cannot be applied to LIA/LRA/etc.

[NikolajBjorner]

psat and qffd check abstractions of these kinds of formulas