diff --git a/bench/ce-bench b/bench/ce-bench
index 5bc80ac29587b1f84fc88a1cfa6c151154157adc..d5c86f986514c9aacf7c60f5b3194ff9dd08e534 100755
--- a/bench/ce-bench
+++ b/bench/ce-bench
@@ -4,6 +4,7 @@ dir=`dirname $0`
 
 updateoracle=false
 files=""
+success=true
 
 while test $# != 0; do
 case "$1" in
@@ -44,6 +45,7 @@ run () {
             echo "FAILED!"
             echo "diff is the following:"
             diff "$f.oracle" "$f.out"
+            success=false
         fi
     fi
 }
@@ -57,3 +59,8 @@ for file in $files; do
     run CVC4,1.5 $filedir/$filebase
     run Z3,4.6.0 $filedir/$filebase
 done
+if $success; then
+    exit 0
+else
+    exit 1
+fi
diff --git a/bench/ce/floats_CVC4,1.5.oracle b/bench/ce/floats_CVC4,1.5.oracle
index b78e29ab16b97f3e9ad2be053aa6dd3eb3fa526e..be00964dc96c65865ee1225d9db89e780d29950e 100644
--- a/bench/ce/floats_CVC4,1.5.oracle
+++ b/bench/ce/floats_CVC4,1.5.oracle
@@ -1,120 +1,120 @@
 bench/ce/floats.mlw T32 g1: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g2: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g3: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g4: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g5: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g6: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g7: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g8: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g9: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T32 g10: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g1: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g2: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g3: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g4: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g5: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g6: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g7: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g8: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g9: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
 bench/ce/floats.mlw T64 g10: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "-1" }
 
diff --git a/bench/ce/floats_Z3,4.6.0.oracle b/bench/ce/floats_Z3,4.6.0.oracle
index 01dd18ff51e045d8b617066270a410081abb1dd8..4a739da8e1d87257dc1fca48a43e7e29cef9d2b9 100644
--- a/bench/ce/floats_Z3,4.6.0.oracle
+++ b/bench/ce/floats_Z3,4.6.0.oracle
@@ -1,6 +1,6 @@
 bench/ce/floats.mlw T32 g1: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -11,7 +11,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g2: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -22,7 +22,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g3: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -32,7 +32,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g4: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -43,7 +43,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g5: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -54,7 +54,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g6: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -64,7 +64,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g7: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -75,7 +75,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g8: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -85,7 +85,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g9: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -96,7 +96,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T32 g10: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -107,7 +107,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g1: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -118,7 +118,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g2: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -129,7 +129,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g3: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -139,7 +139,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g4: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -150,7 +150,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g5: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -161,7 +161,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g6: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -171,7 +171,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g7: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -182,7 +182,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g8: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -192,7 +192,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g9: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw:
@@ -203,7 +203,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
 
 bench/ce/floats.mlw T64 g10: Timeout
 Counter-example model:File ieee_float.mlw:
-Line 218:
+Line 222:
 max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
 "val" : "5" }
 File floats.mlw: