diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index c901f4e57fdd9ee761e50454ef2e064e1fdcb369..001fd13733c7bc716bbd328f821508937546345e 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -3380,22 +3380,29 @@ div_mod_int_bis(A, B, Q, BQ, R) :-
 check_exists_div_mod_int(A,B,Q,BQ,R) :-
     get_saved_cstr_suspensions(LSusp),
     ((member((Susp,div_mod_int(V1,V2,Quot,V2Quot,RR)),LSusp),
-      once (V1 == A; V2 == B),
       (V2 == B ->
           (V1 == A;
            Quot == Q,
            RR == R)
       ;   V1 == A,
           Quot == Q,
-          RR == R))
+          RR == R,
+          (not_unify(Q,0) ->
+              true
+          ;   exists_diff_Rel(V2,B),
+              ZQ = 1)))
     ->
         !,
-        kill_suspension(Susp),
-        protected_unify(A,V1),
-        protected_unify(B,V2),
-        protected_unify(Quot,Q),
-        protected_unify(V2Quot,BQ),
-        protected_unify(Rem,R)
+        (nonvar(ZQ) ->
+            protected_unify(Q,0),
+            protected_unify(BQ,0),
+            protected_unify(V2Quot,0)
+        ;   kill_suspension(Susp),
+            protected_unify(A,V1),
+            protected_unify(B,V2),
+            protected_unify(Quot,Q),
+            protected_unify(V2Quot,BQ),
+            protected_unify(Rem,R))
     ;   % issue 40: cas diviseur <> 0
         % abs(X) = abs(A), abs(Y) = abs(B) =>
         %   abs(X // Y) = abs(A // B) et abs(X rem Y) = abs(A rem B)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index edb8d1ab39c7e6700661754c58280a5bc1e12abf..06846a92ff5bb2a1771cfba625a18a0f936ee88d 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -730,8 +730,8 @@ smt_test :-
 
 smt_test(TO,Size) :-
     %StrDir = "./colibri_tests/colibri/tests/",
-    StrDir = "./colibri_tests/colibri/tests/sat/", %0 (sans real/float-> int!)
-    %StrDir = "./colibri_tests/colibri/tests/unsat/", %0
+    %StrDir = "./colibri_tests/colibri/tests/sat/", %0 (sans real/float-> int!)
+    StrDir = "./colibri_tests/colibri/tests/unsat/", %0
     %StrDir = "./colibri_tests/colibri/tests/unknown/",
     %StrDir = "./colibri_tests/colibri/tests/timeout/",
 
diff --git a/Src/COLIBRI/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index cad874d219226f8158b624d563fde9840e5bf47e..a713d7e441d8320d1498236a8158eef62a181e20 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -1239,9 +1239,9 @@ lin_mult_int(A,B,C) :-
     (Vars = [V,_|_] ->
         ((get_lin_cstrs(V,Cstrs),
           member(mult_int(X,Y,Z),Cstrs),
-          (occurs(0,(X,Y,Z)) ->
-              match_com_binop(A,B,C,X,Y,Z,U1,U2)
-          ;   match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)))
+          (not_unify(C,0) ->
+              match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)
+          ;   match_com_binop(A,B,C,X,Y,Z,U1,U2)))
         ->
             protected_unify(U1 = U2)
         ;   ls_setup,
@@ -1270,7 +1270,9 @@ lin_mult_real(Type,A,B,C) :-
     (Vars = [V,_|_] ->
         ((get_lin_cstrs(V,Cstrs),
           member(mult_real(Type,X,Y,Z),Cstrs),
-          (Type == real ->
+          ((Type == real,
+            not_unify(C,0.0))
+          ->
               match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)
           ;   match_com_binop(A,B,C,X,Y,Z,U1,U2)))
         ->
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index a0eaff17ee3115e6328bc4b6fb93487f24c6fce8..4fb7beeefb31641c213b7277dc8f874a4c69934e 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -12836,7 +12836,8 @@ idiv_mod_real(A,B,Q,R) :-
           (AA == A;
            QQ == Q,
            RR == R)
-      ;    AA == A,
+      ;    not_zero(Q),
+           AA == A,
            QQ == Q,
            RR == R))
     ->
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index c50d6c6218e5a98824c6a7c541aacf099e041b0e..cbd5ae28cb2bed4ca23bd49e8809042db83c75c0 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -10420,12 +10420,21 @@ check_exists_cdiv_crem(A,B,Q,R,Suspend) :-
            R == RR)
       ;   A == AA,
           Q == QQ,
-          R == RR))
-    ->
-        protected_unify(A,AA),
-        protected_unify(B,BB),
-        protected_unify(Q,QQ),
-        protected_unify(R,RR)
+          R == RR,
+          (not_zero(Q) ->
+              true
+          ;   exists_diff_Rel(B,BB),
+              ZQ = 1)))
+    ->
+        (nonvar(ZQ) ->
+            Suspend = 1,
+            protected_unify(Q,0),
+            protected_unify(QQ,0)
+        ;   % Factorisation
+            protected_unify(A,AA),
+            protected_unify(B,BB),
+            protected_unify(Q,QQ),
+            protected_unify(R,RR))
     ;   % issue 40: cas diviseur <> 0
         % abs(X) = abs(A), abs(Y) = abs(B) =>
         %   abs(X // Y) = abs(A // B) et abs(X rem Y) = abs(A rem B)
diff --git a/tests/sat/bug_factorization_urem_udiv.smt2 b/tests/sat/bug_factorization_urem_udiv.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..97e6dff85c081fd1d9d623455dc8e5f2fd5f8bfe
--- /dev/null
+++ b/tests/sat/bug_factorization_urem_udiv.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const x (_ BitVec 512))
+(declare-const y (_ BitVec 512))
+(declare-const z (_ BitVec 512))
+
+(assert (= (bvurem x y) (bvurem x z)))
+(assert (= (bvudiv x y) (bvudiv x z)))
+
+(assert (not (= y z)))
+
+(check-sat)