From c4beb7054bff4bf92da437f288f7027f1d82f705 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 22 Jul 2016 16:51:45 +0200
Subject: [PATCH] spurious assertion

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

diff --git a/src/core/internal.ml b/src/core/internal.ml
index f66ec0b6..4863a0cd 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -1243,7 +1243,6 @@ module Make
       (* Clear hypothesis not valid anymore *)
       for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do
         let c = Vec.get env.clauses_hyps i in
-        assert c.attached;
         assert (c.c_level > l);
         detach_clause c
       done;