Completeness regression in NIA with div

[maurobringolf]

Maybe related to #5338 (but not fixed by its fix).

Commit: 2138ef2

$ z3-4.8.10 unknown.smt2
unsat
$ z3 unknown.smt2
unknown
$ cat unknown.smt2
(assert (forall ((v Int)) (distinct 0 (div 0 v))))
(check-sat)

[maurobringolf]

And a variation:

$ z3-4.8.10 unknown.smt2
unsat
$ z3 unknown.smt2
unknown
$ cat unknown.smt2
(assert (forall ((_ Int)) (= 0 _)))
(assert (= 0 (div 0 0)))
(check-sat)

[NikolajBjorner]

these are butterflies too.
I don't understand a rationale from these tests for dealing with them.
They are out of scope of legacy MBQI completeness claims and they get handled by new core so take up resources to examine.