Debug branch: Assertion violation File: ../src/math/lp/lar_solver.cpp Line: 2252 b.is_int()

[wintered]

Hi,
on the following formula Z3 throws an assertion violation

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (<= (+ (* 1 c) (* 4 b)) 0.8))
(assert (> (* 3 a a) (- (* c 13) 3) 0))
(check-sat)

ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 2252
b.is_int()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: e0411c1

[levnach]

Fixed by c86028b