diff --git a/src/lib/HashConsing.ml b/src/lib/HashConsing.ml
index a7e88dee447e90c162e6de2702c93d99704522c0..6b75c0b9ee40f79c227f74b8b2096b6dce97dd83 100644
--- a/src/lib/HashConsing.ml
+++ b/src/lib/HashConsing.ml
@@ -208,11 +208,18 @@ module Make(H : HashedTyped) : (S with type nde = H.nde and type fml = H.fml) =
           let ndeN = H.negNde nde in
           let hkeyN = realhash ndeN in
           let fmlN = H.toFml ndeN in
-          let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
-          nd.neg <- ndN;
           let idxN = hkeyN mod ds in
-          data.(idxN) <- ndN :: data.(idxN);
-          hc.size <- osize + 2;
+          let bucketN = data.(idxN) in
+          try begin
+            find ndeN bucketN;
+            hc.size <- succ osize;
+          end
+          with Not_found ->
+            let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
+            nd.neg <- ndN;
+            let idxN = hkeyN mod ds in
+            data.(idxN) <- ndN :: data.(idxN);
+            hc.size <- osize + 2
         else hc.size <- succ osize;
         if hc.size > ds lsl 1 then resize hc else ();
         nd