(declare-fun a () Real)
(declare-fun b () Real)
(assert (distinct (mod (to_int (/ a b)) 3) 1))
(check-sat-using purify-arith)

Failed to verify: d->get_range() == m.get_sort(e)
ASSERTION VIOLATION
File: ../src/tactic/generic_model_converter.cpp
Line: 36
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB