Regression in 4.8.3

[yav]

The following example demonstrates a regression, that seems to appear first in version 4.8.3:

(declare-fun f ((Int)) Int
(declare-fun L () Int)
(declare-fun w () Int)

(assert (>= w 1))
(assert (>= L 0))
(assert (>= w (f L))) ; comment out to get an answer (but slower than before)

(assert (not  (<= (* (div L (* 2 w)) (* 2 w)) L)))
(check-sat)

Symptoms:

• Previously, Z3 could solve this immediately, coming up with unsat.
• Versions starting with 4.8.3 don't seem to stop, although I didn't wait very long.
• If you comment out the marked line, which is not needed to complete the proof, then Z3 manages to come up with unsat, but it is much slower than in previous versions.

[NikolajBjorner]

Seems as a reasonable case for expanding division lemmas. One helpful lemma is added where the divisor is positive.

[NikolajBjorner]

There are very likely other useful lemmas that should be instantiated when I see a non-linear div. This is one of them.