diff --git a/bench/ce/jlamp0.mlw b/bench/ce/jlamp0.mlw
index 40d952593f794da52bb9c6cf413590d64a3a61ab..8be63b3030e2debd1d8232fec5dcac2f17dc6bc8 100644
--- a/bench/ce/jlamp0.mlw
+++ b/bench/ce/jlamp0.mlw
@@ -8,10 +8,9 @@ module M
   let p1 (b : ref int)
     requires { 0 <= !a <= 10 /\ 3 <= !b <= 17 }
     ensures  { 17 <= !a <= 42 }
-  =
-    a.contents <- !a + !b;
-    (*assert { 5 <= !a <= 15 };*)
-    (*if !a >= 10 then a.contents <- !a - 1*) ()
+  = a := !a + !b;
+    assert { 5 <= !a <= 15 };
+    if !a >= 10 then a := !a - 1
 
   val c : ref int
 
diff --git a/bench/ce/jlamp0_CVC4,1.5.oracle b/bench/ce/jlamp0_CVC4,1.5.oracle
index 53d42ca669842a72300cdc337208b21f7fb4c955..65bb361763ea19272190476ed01261c7fd8b3554 100644
--- a/bench/ce/jlamp0_CVC4,1.5.oracle
+++ b/bench/ce/jlamp0_CVC4,1.5.oracle
@@ -6,22 +6,55 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 Line 8:
 b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
 "val" : "3" }
-Line 10:
+Line 11:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 Line 12:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 
+bench/ce/jlamp0.mlw M VC p1: Unknown (unknown)
+Counter-example model:File jlamp0.mlw:
+Line 6:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "7" }
+Line 8:
+b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
+"val" : "3" }
+Line 10:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "9" }
+Line 11:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "10" }
+Line 13:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "9" }
+
+bench/ce/jlamp0.mlw M VC p1: Unknown (unknown)
+Counter-example model:File jlamp0.mlw:
+Line 6:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "2" }
+Line 8:
+b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
+"val" : "3" }
+Line 10:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "5" }
+Line 11:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "5" }
+
 bench/ce/jlamp0.mlw M VC p2: Unknown (unknown)
 Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 23:
+Line 22:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
 
@@ -31,20 +64,20 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "2" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "4" }
-Line 26:
+Line 25:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "5" }
-Line 27:
+Line 26:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "4" }
 
@@ -53,21 +86,21 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "10" }
-Line 23:
+Line 22:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "12" }
-Line 26:
+Line 25:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "13" }
-Line 27:
+Line 26:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "12" }
 
@@ -76,21 +109,21 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "9" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "2" }
-Line 24:
+Line 23:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "11" }
-Line 26:
+Line 25:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "11" }
-Line 27:
+Line 26:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "4" }
 
@@ -99,13 +132,13 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 20:
+Line 19:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
diff --git a/bench/ce/jlamp0_Z3,4.6.0.oracle b/bench/ce/jlamp0_Z3,4.6.0.oracle
index 06c5aaddf037529047f43d129f47bcb759467813..b9d6e8973996f230956b0cd029c3755a79af5046 100644
--- a/bench/ce/jlamp0_Z3,4.6.0.oracle
+++ b/bench/ce/jlamp0_Z3,4.6.0.oracle
@@ -6,22 +6,55 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 Line 8:
 b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
 "val" : "3" }
-Line 10:
+Line 11:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 Line 12:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 
+bench/ce/jlamp0.mlw M VC p1: Timeout
+Counter-example model:File jlamp0.mlw:
+Line 6:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "7" }
+Line 8:
+b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
+"val" : "3" }
+Line 10:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "9" }
+Line 11:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "10" }
+Line 13:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "9" }
+
+bench/ce/jlamp0.mlw M VC p1: Timeout
+Counter-example model:File jlamp0.mlw:
+Line 6:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "2" }
+Line 8:
+b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
+"val" : "3" }
+Line 10:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "5" }
+Line 11:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
+"val" : "5" }
+
 bench/ce/jlamp0.mlw M VC p2: Timeout
 Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 23:
+Line 22:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
 
@@ -31,20 +64,20 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "2" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "4" }
-Line 26:
+Line 25:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "5" }
-Line 27:
+Line 26:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "4" }
 
@@ -53,21 +86,21 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "10" }
-Line 23:
+Line 22:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "12" }
-Line 26:
+Line 25:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "13" }
-Line 27:
+Line 26:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "12" }
 
@@ -76,21 +109,21 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "9" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "2" }
-Line 24:
+Line 23:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "11" }
-Line 26:
+Line 25:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "11" }
-Line 27:
+Line 26:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "4" }
 
@@ -99,13 +132,13 @@ Counter-example model:File jlamp0.mlw:
 Line 6:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "0" }
-Line 20:
+Line 19:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
-Line 21:
+Line 20:
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
 "val" : "1" }
-Line 22:
+Line 21:
 a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
 "val" : "3" }
 c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,