diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 9c18bdbd..0e27a550 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -1500,7 +1500,6 @@ module Make(Plugin : PLUGIN)
           )
         )
     with Trivial ->
-      Vec.push vec init;
       Log.debugf info (fun k->k "Trivial clause ignored : @[%a@]" Clause.debug init)
 
   let[@inline never] flush_clauses_ st =