ASSERTION VIOLATION File: ../src/util/mpq.h Line: 538

[wingsyuyi-satori]

Hello, I encountered an assertion violation when running Z3 debug build on the following input.
Input :

(declare-const r (_ BitVec 8))
(declare-const t (_ BitVec 8))
(assert (and (= t ((_ int_to_bv 8) (div (+ (ubv_to_int (bvadd r t)) 130) 2))) (not (= t (_ bv0 8)))))

Output :

ASSERTION VIOLATION
File: ../src/util/mpq.h
Line: 538
is_int(a) && is_int(b)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB, Invoke (L)LDB

Commit : ec42464

[NikolajBjorner]

 	z3.exe!mpq_manager<1>::rem(const mpq & a, const mpq & b, mpq & c) Line 538	C++
 	z3.exe!operator%(const rational & r1, const rational & r2) Line 285	C++
 	z3.exe!lp::dioph_eq::imp::tighten_bounds_for_non_trivial_gcd(const rational & g, unsigned int j, bool is_upper) Line 1778	C++
>	z3.exe!lp::dioph_eq::imp::tighten_on_espace(unsigned int j) Line 1632	C++
 	z3.exe!lp::dioph_eq::imp::subs_qfront_by_S(unsigned int k, lp::dioph_eq::imp::protected_queue & q, unsigned int j) Line 1322	C++
 	z3.exe!lp::dioph_eq::imp::subs_front_with_S_and_fresh(lp::dioph_eq::imp::protected_queue & q, unsigned int j) Line 1399	C++

[levnach]

Fixed with 17dffc6. There was a conflict created very early in the dioph_eq::check() that should be caught but instead the algorithm worked with a term with a fractional free coefficient, that caused the assert.