% z3-752b498 smt.arith.solver=6 bug.smt2
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
sat
% cat bug.smt2
(declare-fun a () Int) 
(declare-fun b () Int) 
(declare-fun c () Int) 
(assert (let ((?d c)) 
        (and (<= (+ a (* 6 b))(/ 8 101 ))
        (<= (* ?d a) (- 4 (* 6 a)) 0)))) 
(check-sat)