From ac706f3e56f0196f720e56a2d7d60be3b7d846d1 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 28 Jul 2016 10:18:07 +0200
Subject: [PATCH] fix bug

---
 src/core/internal.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index b3e6085f..2142b26e 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -1134,6 +1134,8 @@ module Make
     if is_unsat () then raise Unsat;
     let n_of_conflicts = ref (to_float env.restart_first) in
     let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
+    (* return to level 0 before pushing assumptions *)
+    cancel_until 0;
     push_assumptions assumptions;
     assert (env.base_level <= List.length assumptions);
     try