[SMT-LIB] The "rem" operator

[Delcypher]

Hi,

I've been playing around with Z3 recently and I noticed that supports
the "rem" operator which doesn't seem to be part of SMTLIB.

Example:

```
(set-option :produce-models true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun rem_result () Int)
(declare-fun div_result () Int)
(declare-fun mod_result () Int)
(assert (= a 12))
(assert (= b (- 7)))
(assert (= rem_result (rem a b)))
(assert (= mod_result (mod a b)))
(assert (= div_result (div a b)))
(check-sat)
(get-model)
sat
(model
  (define-fun div_result () Int
    (- 1))
  (define-fun mod_result () Int
    5)
  (define-fun rem_result () Int
    (- 5))
  (define-fun b () Int
    (- 7))
  (define-fun a () Int
    12)
)
```

I've noted that CVC4 doesn't support "rem" so I'm guessing it's a Z3
extension. Are there any plans to make it an official part of SMTLIB?

It seems strange that QF_BV has both "bvsmod" and "bvsdiv" but the
logics that use Integers only have "mod". However I'm quite ignorant
of the distinction between "mod" and "rem" but clearly there is a
difference.

I noticed that "div" and "mod" uses the "Euclidean" definition of
division but how about "rem", "bvsmod" and "bvsdiv"? Is there name
given to definition that's used these?

Thanks,
Dan Liew.