From 30842da94776938d67fdc6400ed4d2b70ebdeca0 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Sat, 30 Jan 2016 17:03:14 +0100
Subject: [PATCH] Fixed refreshing of clauses with push/pop

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

diff --git a/solver/internal.ml b/solver/internal.ml
index b6a81f6b..bd584628 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -1097,7 +1097,7 @@ module Make
         if c.c_level > l then begin
           remove_clause c;
           match c.cpremise with
-          | History [ { cpremise = Lemma _ } as c' ] -> Stack.push c' s
+          | History ({ cpremise = Lemma _ } as c' :: _ ) -> Stack.push c' s
           | _ -> () (* Only simplified clauses can have a level > 0 *)
         end else begin
           Log.debugf 15 "Keeping intact clause %a" (fun k->k St.pp_clause c);