Hi,
For this formula:
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (<= c a b d a))
(assert (= (/ 0 c) (+ (* a d) b)))
(check-sat)
Z3 debug branch throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1710
m_term_register.size() == m_terms.size()
(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