purify-arith Assertion violation at ../src/tactic/generic_model_converter.cpp Line: 36

[muchang]

Hi,
For this formula,

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

z3 throws out an assertion violation:

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

OS: Ubuntu 18.04
Revision: d02d90d

[NikolajBjorner]

Given the deluge of these fuzz reports and the effort involved with tracking regressions:
Could you also add a pull request with "issue-2976.smt2.open" to z3test/regressions/smt2
and similar issues? While it is valuable to fix the many corner cases and the bug-minimization is appreciated, it also takes up resources to triage and fix and currently I don't have bandwidth to update the regression suite with these issues.

[muchang]

Sure, I will add the test cases to the regression test suite soon.