Debug branch: Assertion violation at ../src/math/lp/nla_order_lemmas.cpp Line: 343

[muchang]

Hi,
For this formula:

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(assert (< (+ (* (+ 2 a) (- (- 2) b) (* 30 c)) e) 0))
(assert (> (/ 50 d e) 40))
(assert (<= (+ 20 a b) c 60 d))
(assert (>= e 2))
(check-sat)

Z3 debug branch throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/math/lp/nla_order_lemmas.cpp
Line: 343
sign * val(m) < val(a) * val(b)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: d68c114

[levnach]

Fixed by f088932