Assertion violation at math/lp/lar_solver.cpp:2252

[wintered]

% 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)

OS: Ubuntu 18.04
Commit: 752b498

[NikolajBjorner]

I think I have mentioned this many times by now: fuzz bugs that set arith.solver=6 and establish an issue in the master branch are not useful. THe Debug branch tracks latest development of arith.solver=6, and bugs there are welcome, but not in the master branch. We have on purpose only selectively enabled arith.solver=6 at this point and fuzz bugs that play with the parameter are not interesting.