Assertion violation at sat_local_search.cpp:240 (add-bounds card2bv normalize-bounds qfnia)

[rainoftime]

Hi, for the following formula,

(set-logic QF_UFNIA)
(set-option :sat.local_search true)
(declare-const i0 Int)
(declare-const i2 Int)
(declare-const v13 Bool)
(assert (or (>= i0 (* 355 85 361 i2 63)) v13))
(check-sat-using (then simplify add-bounds card2bv normalize-bounds qfnia))

z3 (commit dc9221e) throws an assertion violation

Failed to verify: c.m_k < constraint_value(c)
ASSERTION VIOLATION
File: ../src/sat/sat_local_search.cpp
Line: 240
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB