Assertion violation at theory_utvpi_def.h:802

[rainoftime]

Hi, for this formula

(set-logic QF_AUFNIA)
(set-option :model_validate true)
(set-option :smt.arith.solver 4)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i11 Int)
(assert (< i11 i5))
(assert (> i6 i5))
(check-sat-using ctx-solver-simplify)

z3 f447292 throws an assertion violation

File: theory_utvpi_def.h:802
Line: 802
m_graph.is_feasible()

[rainoftime]

There is no warning like "found non utvpi logic expression".
And I think the assertions below belong to UTVPI.

(assert (< i11 i5))
(assert (> i6 i5))

So I report this issue.

[NikolajBjorner]

it is a simpler repro for #3573

[NikolajBjorner]

feel empowered to copy the bug report to #3573

[rainoftime]

Merged to #3573