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
Hi,
For this formula:
Z3 debug branch throws out an assertion violation:
OS: Ubuntu 18.04
Commit: caa118c