diff --git a/colibri2/tests/solve/smt_nra/sat/dune.inc b/colibri2/tests/solve/smt_nra/sat/dune.inc
index 2aa3fb3dc46f72f2727e517137bf675826800483..1a70924bdcc3bfc2baeaaff7786faf5c142b3485 100644
--- a/colibri2/tests/solve/smt_nra/sat/dune.inc
+++ b/colibri2/tests/solve/smt_nra/sat/dune.inc
@@ -20,5 +20,8 @@
 --dont-print-result %{dep:mul_pos_lt.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos_lt.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:mul_zero.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_zero.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:sqrt_tower.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:sqrt_tower.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_nra/sat/mul_zero.smt2 b/colibri2/tests/solve/smt_nra/sat/mul_zero.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..c7ca4b6855dfdd20630609071a16b5566d0974f3
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/sat/mul_zero.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+
+(declare-fun a () Real)
+(declare-fun b () Real)
+
+(assert (= 0.0 (* a b)))
+(assert (distinct a b))
+
+(check-sat)
diff --git a/colibri2/tests/solve/smt_nra/unsat/dune.inc b/colibri2/tests/solve/smt_nra/unsat/dune.inc
index 8cda5df03dec65ba3e8f0644b07dc06c0d330043..b0cbe92787be6f4c201d221d56fc6b969e2d71de 100644
--- a/colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -38,6 +38,9 @@
 --dont-print-result %{dep:mult_sqrt_hard.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mult_sqrt_hard.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:product_subst_zero_in_denominator.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:product_subst_zero_in_denominator.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:sqrt.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:sqrt.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
diff --git a/colibri2/tests/solve/smt_nra/unsat/product_subst_zero_in_denominator.smt2 b/colibri2/tests/solve/smt_nra/unsat/product_subst_zero_in_denominator.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..997a5602e689172f4e49871fb7e32e4c73c29c3a
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/unsat/product_subst_zero_in_denominator.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(assert (forall ((x Real) (y Real) (z Real)) (= (/ z (+ x y)) (+ z (/ 1.0 z)))))
+(define-fun n ((z Real) (y Real)) Bool (< z 0.0))
+(declare-fun m () Real)
+(declare-fun r (Real) Real)
+(assert (forall ((x Real) (y Real)) (ite (n x 0.0) true (n (r y) x))))
+(assert (or (not (n (r 0.0) m)) (= 0.0 (/ (+ m 1) (+ m 1)))))
+(check-sat)
diff --git a/colibri2/theories/LRA/dom_product.ml b/colibri2/theories/LRA/dom_product.ml
index 8093a36ca887219e0871f16d7891d17bad5d3c38..b6da81b36c4ebc321d1e0d585c8283590254a258 100644
--- a/colibri2/theories/LRA/dom_product.ml
+++ b/colibri2/theories/LRA/dom_product.ml
@@ -141,13 +141,16 @@ end = Pivot.WithUnsolved (struct
   let solve (_, notz1, unk1, p1) (_, notz2, unk2, p2) :
       _ Pivot.solve_with_unsolved =
     let exception Solved of Node.t * Product.t in
-    let all_zero (p : Product.t) : _ Pivot.solve_with_unsolved =
-      if Node.M.is_empty p.poly then
+    let some_zero unk (p : Product.t) : _ Pivot.solve_with_unsolved =
+      (* Use the one unknown to not be null *)
+      if Node.M.is_empty unk then
         if A.is_zero p.cst then AlreadyEqual else Contradiction
-      else Subst (Node.M.map (fun _ -> Product.zero) p.poly)
+      else if Node.M.is_num_elt 1 unk then
+        Subst (Node.M.map (fun _ -> Product.zero) unk)
+      else Unsolved
     in
-    if Product.is_zero p1 then all_zero p2
-    else if Product.is_zero p2 then all_zero p1
+    if Product.is_zero p1 then some_zero unk2 p2
+    else if Product.is_zero p2 then some_zero unk1 p1
     else if
       Node.M.is_empty notz1 && Node.M.is_empty unk1 && Node.M.is_empty notz2
       && Node.M.is_empty unk2