Debug branch: Assertion violation at ../src/math/lp/gomory.cpp Line: 337

[muchang]

Hi,
For this formula:

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert
 (let ((d 0))
  (and
   (or
    (= (< c a)
     (distinct
      (distinct
       (xor (<= (/ 57 c c) 2) (distinct (distinct c b) (< (/ a c) 5)))
       (distinct c b))
      (xor (<= b a) (>= (- a) 4))))
    (>= (* c a) 51))
   (> a c))))
(check-sat)

Z3 debug branch throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/math/lp/gomory.cpp
Line: 337
lia.current_solution_is_inf_on_cut()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: caa118c

[levnach]

fixed by 7b51b39