diff --git a/sledge/lib/exp.mli b/sledge/lib/exp.mli
index 4244ac02f..9e387d664 100644
--- a/sledge/lib/exp.mli
+++ b/sledge/lib/exp.mli
@@ -50,8 +50,10 @@ type op2 =
   | Add  (** Addition *)
   | Sub  (** Subtraction *)
   | Mul  (** Multiplication *)
-  | Div  (** Division *)
-  | Rem  (** Remainder of division *)
+  | Div  (** Division, for integers result is truncated toward zero *)
+  | Rem
+      (** Remainder of division, satisfies [a = b * div a b + rem a b] and
+          for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
   | Udiv  (** Unsigned division *)
   | Urem  (** Remainder of unsigned division *)
   | And  (** Conjunction, boolean or bitwise *)
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index 69ea56977..ba24c85ae 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -35,8 +35,10 @@ type op2 =
   | Le  (** Less-than-or-equal test *)
   | Ord  (** Ordered test (neither arg is nan) *)
   | Uno  (** Unordered test (some arg is nan) *)
-  | Div  (** Division *)
-  | Rem  (** Remainder of division *)
+  | Div  (** Division, for integers result is truncated toward zero *)
+  | Rem
+      (** Remainder of division, satisfies [a = b * div a b + rem a b] and
+          for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
   | And  (** Conjunction, boolean or bitwise *)
   | Or  (** Disjunction, boolean or bitwise *)
   | Xor  (** Exclusive-or, bitwise *)