From 8afdc59ced1c1e17342b18aa0af58004112d27a5 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Sat, 24 Jan 2015 21:24:03 +0100
Subject: [PATCH] Tentative fix for absurd slice size

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

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 05ccc60c..ef0f2fd0 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -638,7 +638,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
     })
 
   let rec theory_propagate () =
-    let head = Vec.size env.trail in
+    let head = env.qhead in
+    L.debug 5 "Propagating to theory (with head = %d)" head;
     match Th.assume (current_slice ()) with
     | Th.Sat ->
       L.debug 5 "env.tatoms_qhead : %d -> %d" env.tatoms_qhead head;