Fortress

Про это подробно не пишут (во всяком случае я пока не нашёл). Но разница есть (возникает при работе с отрицательными числами) и следующий пример её демонстрирует:

(declare-const a Int)
(declare-const b Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(assert (= a 10))
(assert (= b 4))

(assert (= r1 (mod a b))) ; mod
(assert (= r2 (rem a b))) ; remainder
(assert (= r3 (mod a (- b)))) ; mod
(assert (= r4 (rem a (- b)))) ; remainder

(check-sat)
(get-value (a b r1 r2 r3 r4))

sat
((a 10)
 (b 4)
 (r1 2)
 (r2 2)
 (r3 2)
 (r4 (- 2)))

Z3 реализует следующее поведение (выяснено методом тыка):

1. MOD всегда дает положительный результат независимо от знака операндов;
2. REM даёт отрицательный результат только если второй операнд отрицателен, знак первого не влияет на результат.

В Java сделано следующим образом (выяснено методом тыка):

1. MOD знак результата зависит от знака второго операнда, знак первого игнорируется
2. REM такого оператора нет