diff --git a/solver/internal.ml b/solver/internal.ml
index 99a89f4a..40b049bb 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -317,7 +317,6 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl);
     end;
     assert (Vec.size env.trail_lim = Vec.size env.tenv_queue);
-    assert (env.qhead = Vec.size env.trail);
     ()
 
   let report_unsat ({atoms=atoms} as confl) =