From 63d8dc1dc221e2f4dae2f986e936df9e95a11361 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 15 Apr 2016 12:49:38 +0200
Subject: [PATCH] [bugfix/major] Clauses can be added at level > 0

---
 solver/internal.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/solver/internal.ml b/solver/internal.ml
index c10c38c2..9a98b2bb 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -858,6 +858,7 @@ module Make
       if satisfied c then remove_clause c
     done
 
+(*
   let simplify () =
     assert (decision_level () = 0);
     if is_unsat () then raise Unsat;
@@ -873,6 +874,7 @@ module Make
       env.simpDB_assigns <- Vec.size env.elt_queue;
       env.simpDB_props <- env.clauses_literals + env.learnts_literals;
     end
+*)
 
   (* Decide on a new litteral *)
   let rec pick_branch_aux atom =
@@ -956,8 +958,11 @@ module Make
     let aux cl =
       let c = make_clause ?tag (fresh_hname ()) cl (List.length cl) false (History []) (current_level ()) in
       add_clause c;
+      (* Clauses can be added after search has begun (and thus we are not at level 0,
+         so better not do anything at this point.
       match propagate () with
       | None -> () | Some confl -> report_unsat confl
+      *)
     in
     List.iter aux cnf