From a5c67c75450831e27356e30f888e19cb667ac2af Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 26 Jan 2015 15:54:28 +0100
Subject: [PATCH] Fix for lack of insertion of new atoms in iheap.

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

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 25bf2688..65b66b90 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -650,6 +650,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
       propagate ()
     | Th.Unsat (l, p) ->
       let l = List.rev_map new_atom l in
+      List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l;
       let c = St.make_clause (St.fresh_name ()) l (List.length l) true (Lemma p) in
       Some c