smt.diff_logic: non-diff logic expression

[DKLoehr]

When giving this file as input to z3 4.8.6, I get the error

(smt.diff_logic: non-diff logic expression [...]

followed by a very large expression. Searching through the expression reveals several instances of multiplication by -1, which are not present in the original file, leading me to suspect a z3 bug. This appears to be the same as, or very similar to, #1266. As was the case there, I haven't been able to reproduce the bug on any smaller input files.

Removing the use of solve-eqs from the final line avoids the issue, but results in significantly increased solving times. This file is very slightly smaller and does not yield this error.