From 28f32de24c0f56205fcb6ff7818399130ac52b96 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 18 Nov 2015 17:43:26 +0100
Subject: [PATCH] Removed assertion Long explanation: when backtracking to
 level 0, while already being at level 0, very strange things might happen,
 most notably there might still be facts left to propagate...

---
 solver/internal.ml | 1 -
 1 file changed, 1 deletion(-)

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) =