(simplify, bv) Assertion violation at ../src/math/lp/int_branch.cpp Line: 84

[muchang]

Hi,
For this formula:

(assert (forall ((x Int) (y Int) (z Int)) (= x (/ 1 y z (- 128 z 1)))))
(check-sat-using (then simplify bv))

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/math/lp/int_branch.cpp
Line: 84
!lia.column_is_int_inf(j) || !lia.is_fixed(j)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: a0de244

[levnach]

Does not repro in 97fe2c8