diff --git a/src/HolSmt/SmtLib.sml b/src/HolSmt/SmtLib.sml
index 515fcc2912..2f69cc3f4b 100644
--- a/src/HolSmt/SmtLib.sml
+++ b/src/HolSmt/SmtLib.sml
@@ -567,13 +567,15 @@ in
   fun SIMP_TAC simp_let =
     let
       open Tactical simpLib
-      val INT_ABS = intLib.ARITH_PROVE
-                      ``!x. ABS (x:int) = if x < 0i then 0i - x else x``
+      (* TODO: In the future it'd probably be better to translate the
+         definitions of `ABS`, `int_min`, `int_max`, etc, or any other needed
+         user-defined functions automatically and pass those on to the SMT
+         solver, instead of doing these special-case rewrites here. *)
     in
       REPEAT Tactic.GEN_TAC THEN
       (if simp_let then Library.LET_SIMP_TAC else ALL_TAC) THEN
       SIMP_TAC pureSimps.pure_ss
-        [integerTheory.INT_MIN, integerTheory.INT_MAX, INT_ABS] THEN
+        [integerTheory.INT_MIN, integerTheory.INT_MAX, integerTheory.INT_ABS] THEN
       Library.WORD_SIMP_TAC THEN
       Library.SET_SIMP_TAC THEN
       Tactic.BETA_TAC
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 86c8191def..8841a4a104 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -415,18 +415,18 @@ in
     (``ABS (ABS (x:int)) = ABS x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
     (``ABS (x:int) = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
 
-    (``int_min (x:int) y <= x``, [thm_AUTO, thm_YO]),
-    (``int_min (x:int) y <= y``, [thm_AUTO, thm_YO]),
-    (``(z:int) < x /\ z < y ==> z < int_min x y``, [thm_AUTO, thm_YO]),
+    (``int_min (x:int) y <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``int_min (x:int) y <= y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(z:int) < x /\ z < y ==> z < int_min x y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``int_min (x:int) y < x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``int_min (x:int) 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:int) >= 0 ==> (int_min x 0 = 0)``, [thm_AUTO, thm_YO]),
+    (``(x:int) >= 0 ==> (int_min x 0 = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``int_max (x:int) y >= x``, [thm_AUTO, thm_YO]),
-    (``int_max (x:int) y >= y``, [thm_AUTO, thm_YO]),
-    (``(z:int) > x /\ z > y ==> z > int_max x y``, [thm_AUTO, thm_YO]),
+    (``int_max (x:int) y >= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``int_max (x:int) y >= y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(z:int) > x /\ z > y ==> z > int_max x y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``int_max (x:int) y > x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:int) >= 0 ==> (int_max x 0 = x)``, [thm_AUTO, thm_YO]),
+    (``(x:int) >= 0 ==> (int_max x 0 = x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (* real *)