diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 5eb06b9b85..de57ab8ed2 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -425,6 +425,55 @@ in
     (``(x:int) < 0 ==> (x / ~1 = ~x / 1)``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
+    (``(~42:int) quot ~42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot ~42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) quot ~1 = 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot ~1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot ~1 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot ~1 = ~42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) quot 1 = ~42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot 1 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot 1 = 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) quot 42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot 42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot ~1 = ~x``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot 42 <= x``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 42 <= ABS x``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3_v4, thm_Z3p_v4]),
+    (``((x:int) quot 42 = x) = (x = 0)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot 42 = x <=> x = 0 \/ x = ~1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 0 = x``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) quot 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) quot 0 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) quot 0 = 1 quot 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 0 = x quot 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+
+    (* cf. integerTheory.int_quot *)
+    (``(x:int) < 0 ==> (x quot 1 = ~(~x quot 1))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) < 0 ==> (x quot 42 = ~(~x quot 42))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``0 <= (x:int) ==> (x quot ~42 = ~(x quot 42))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``0 <= (x:int) ==> (x quot ~1 = ~(x quot 1))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) < 0 ==> (x quot ~42 = ~x quot 42)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) < 0 ==> (x quot ~1 = ~x quot 1)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+
     (``(~42:int) % ~42 = 0``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) % ~42 = ~1``,
@@ -487,6 +536,50 @@ in
     (``(x:int) % 42 = x - x / 42 * 42``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
+    (``(~42:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem ~42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem ~42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem 42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem 42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 42 < 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``((x:int) rem 42 = x) = (x < 42)``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``((x:int) rem 42 = x) <=> (0 <= x) /\ (x < 42)``,
+      [sat_CVC, sat_Z3, sat_Z3p]),
+    (``((x:int) rem 42 = x) <=> (-42 < x) /\ (x < 42)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 0 = x``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) rem 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) rem 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) rem 0 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) rem 0 = x rem 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+
+    (* cf. integerTheory.int_rem *)
+    (``(x:int) rem ~42 = x - x quot ~42 * ~42``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem ~1 = x - x quot ~1 * ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 1 = x - x quot 1 * 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 42 = x - x quot 42 * 42``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+
     (``ABS (x:int) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
     (``(ABS (x:int) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
     (``(x:int) >= 0 ==> (ABS x = x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),