Unsound handling of rem in new release.

[hermanventer]

hermanventer@Hermans-MacBook-Pro MIRAI % z3 --version
Z3 version 4.10.1 - 64 bit
hermanventer@Hermans-MacBook-Pro MIRAI % which z3
/opt/homebrew/bin/z3
hermanventer@Hermans-MacBook-Pro MIRAI % cat z3.bug
(declare-fun param_1 () Int)
(assert (= 0 (rem param_1 2)))
(assert (let ((a!1 (not (= 0 (rem (- 255 param_1) 2)))))
(not a!1)))
(check-sat)
(get-model)
hermanventer@Hermans-MacBook-Pro MIRAI % z3 z3.bug
sat
(
(define-fun param_1 () Int
0)
)

Needless to say, this used to be unsatisfiable and still is on https://jfmc.github.io/z3-play/

Confirmed that this works as expected (non sat) using 4.9.1

[NikolajBjorner]

it has to be a regression, not specific to M1