diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index ec1d280c702815e5e081007e2dd2a8e22251787c..cb00b0fc14c92612e7d0b0922171bc80f30c017d 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -56,20 +56,17 @@ AC_MSG_CHECKING(for Frama-C version)
 DEV_VERSION_NUMBER=`echo $FRAMAC_VERSION | sed -e 's/.*-\(.*\)/\1/' `
 VERSION_NUMBER=`echo $DEV_VERSION_NUMBER | sed -e 's/\(.*\)+dev/\1/' `
 
-if test $VERSION_NUMBER -lt 20130401; then
-  AC_MSG_ERROR(Frama-C version must be at least Fluorine-20130401.)
-else if test $VERSION_NUMBER -gt 20130501; then
-  AC_MSG_WARN(Frama-C version higher than Fluorine-20130501 not tested: use it at your own risk.)
-fi
+if test $VERSION_NUMBER -lt 20130601; then
+  AC_MSG_ERROR(Frama-C version must be at least Fluorine-20130601.)
 fi
 
 # at the time being, must use the Frama-C development version
-# DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
-# if test "$DEV" != "+dev"; then
-#   AC_MSG_ERROR(Frama-C version must be the current SVN version.);
-# else
+DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
+if test "$DEV" != "+dev"; then
+  AC_MSG_ERROR(Frama-C version must be the current SVN version.);
+else
    AC_MSG_RESULT($FRAMAC_VERSION)
-# fi
+fi
 
 # OCaml version
 ###############
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 7d5b9ba80e6e9c7a6967b7ff4363e8fb40f9168b..9f46401e2f50941934878859763c9e36d359363d 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -380,7 +380,7 @@ module rec Transfer
       | None -> state
       | Some init -> do_init vi init state
     in
-    Globals.Vars.fold_in_file_order do_one state
+    Globals.Vars.fold_in_file_rev_order do_one state
 
   (** The (backwards) transfer function for a branch. The [(Cil.CurrentLoc.get
       ())] is set before calling this. If it returns None, then we have some