From 6005652f3f113768fb58ce1126212c545340e321 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 13 Mar 2015 14:39:48 +0100
Subject: [PATCH] Only pure hypothesis are instantly learned

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

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index f1b981bd..f88f2bb0 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -501,6 +501,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
     L.debug 10 "Adding clause : %a" St.pp_clause init0;
     try
       if Proof.has_been_proved init0 then raise Trivial;
+      assert (Proof.is_proven init0); (* Important side-effect, DO NOT REMOVE *)
       let atoms, init = partition atoms init0 in
       let size = List.length atoms in
       match atoms with
@@ -513,7 +514,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
             else make_clause name atoms size true (History [init0])
         in
         L.debug 1 "New clause : %a" St.pp_clause clause;
-        Proof.prove clause;
         attach_clause clause;
         Vec.push env.clauses clause;
         if a.neg.is_true then begin