diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 8ce7d391..486248b1 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -232,7 +232,7 @@ module Make(Plugin : PLUGIN)
     let[@inline] equal a b = a == b
     let[@inline] sign a = a == abs a
     let[@inline] hash a = Hashtbl.hash a.aid
-    let[@inline] compare a b = Pervasives.compare a.aid b.aid
+    let[@inline] compare a b = compare a.aid b.aid
     let[@inline] reason a = Var.reason a.var
     let[@inline] id a = a.aid
     let[@inline] is_true a = a.is_true
@@ -1871,7 +1871,7 @@ module Make(Plugin : PLUGIN)
     Log.debugf 3 (fun k->k "(@[sat.gc.start :keep %d :out-of %d@])" n_of_learnts (Vec.size v));
     assert (Vec.size v > n_of_learnts);
     (* sort by decreasing activity *)
-    Vec.sort v (fun c1 c2 -> Pervasives.compare c2.activity c1.activity);
+    Vec.sort v (fun c1 c2 -> compare c2.activity c1.activity);
     let n_collected = ref 0 in
     while Vec.size v > n_of_learnts do
       let c = Vec.pop v in
diff --git a/src/sat/Int_lit.ml b/src/sat/Int_lit.ml
index cdac09d4..9f01aaeb 100644
--- a/src/sat/Int_lit.ml
+++ b/src/sat/Int_lit.ml
@@ -44,7 +44,7 @@ let set_sign b i = if b then abs i else neg (abs i)
 
 let hash (a:int) = a land max_int
 let equal (a:int) b = a=b
-let compare (a:int) b = Pervasives.compare a b
+let compare (a:int) b = compare a b
 
 let make i = _make (2 * i)