ASSERTION VIOLATION, File: ../src/math/lp/lar_solver.cpp, Line: 1161

[zhendongsu]

[608] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1161
!column_is_int(j) || v.is_int()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[609] % cat small.smt2
(set-option :smt.arith.ignore_int true)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (< a (* (to_real (mod 0 0)) (ite (< a (* a b) (to_real (mod 0 0))) 2 0)) 0))
(check-sat)