diff --git a/autom4te.cache/output.0 b/autom4te.cache/output.0
index d9e048833b68924637cec160f8992b3aee3e8626..a92523a03602f136f9213d3a40b9d69073c3d09f 100644
--- a/autom4te.cache/output.0
+++ b/autom4te.cache/output.0
@@ -1,6 +1,6 @@
 @%:@! /bin/sh
 @%:@ Guess values for system-dependent variables and create Makefiles.
-@%:@ Generated by GNU Autoconf 2.69 for lustrec 1.1-Unversioned directory.
+@%:@ Generated by GNU Autoconf 2.69 for lustrec 1.3-      55.
 @%:@
 @%:@ Report bugs to <ploc@garoche.net>.
 @%:@ 
@@ -579,8 +579,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='lustrec'
 PACKAGE_TARNAME='lustrec'
-PACKAGE_VERSION='1.1-Unversioned directory'
-PACKAGE_STRING='lustrec 1.1-Unversioned directory'
+PACKAGE_VERSION='1.3-      55'
+PACKAGE_STRING='lustrec 1.3-      55'
 PACKAGE_BUGREPORT='ploc@garoche.net'
 PACKAGE_URL=''
 
@@ -589,10 +589,18 @@ ac_default_prefix=/usr/local
 ac_subst_vars='LTLIBOBJS
 LIB@&t@OBJS
 abs_datadir
+OBJEXT
+EXEEXT
+ac_ct_CC
+CPPFLAGS
+LDFLAGS
+CFLAGS
+CC
 OCAMLBUILD
 OCAMLC
+SRC_PATH
 OCAMLGRAPH_PATH
-SVN_REVISION
+VERSION_CODENAME
 target_alias
 host_alias
 build_alias
@@ -638,7 +646,12 @@ with_ocamlgraph_path
 '
       ac_precious_vars='build_alias
 host_alias
-target_alias'
+target_alias
+CC
+CFLAGS
+LDFLAGS
+LIBS
+CPPFLAGS'
 
 
 # Initialize some variables set by options.
@@ -1179,7 +1192,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures lustrec 1.1-Unversioned directory to adapt to many kinds of systems.
+\`configure' configures lustrec 1.3-      55 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1240,7 +1253,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of lustrec 1.1-Unversioned directory:";;
+     short | recursive ) echo "Configuration of lustrec 1.3-      55:";;
    esac
   cat <<\_ACEOF
 
@@ -1251,6 +1264,18 @@ Optional Packages:
                           should be in ocamlgraph-path @<:@default=@S|@(ocamlfind
                           query ocamlgraph)@:>@
 
+Some influential environment variables:
+  CC          C compiler command
+  CFLAGS      C compiler flags
+  LDFLAGS     linker flags, e.g. -L<lib dir> if you have libraries in a
+              nonstandard directory <lib dir>
+  LIBS        libraries to pass to the linker, e.g. -l<library>
+  CPPFLAGS    (Objective) C/C++ preprocessor flags, e.g. -I<include dir> if
+              you have headers in a nonstandard directory <include dir>
+
+Use these variables to override the choices made by `configure' or to help
+it to find libraries and programs with nonstandard names/locations.
+
 Report bugs to <ploc@garoche.net>.
 _ACEOF
 ac_status=$?
@@ -1314,7 +1339,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-lustrec configure 1.1-Unversioned directory
+lustrec configure 1.3-      55
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -1327,11 +1352,95 @@ fi
 ## ------------------------ ##
 ## Autoconf initialization. ##
 ## ------------------------ ##
+
+@%:@ ac_fn_c_try_compile LINENO
+@%:@ --------------------------
+@%:@ Try to compile conftest.@S|@ac_ext, and return whether this succeeded.
+ac_fn_c_try_compile ()
+{
+  as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
+  rm -f conftest.$ac_objext
+  if { { ac_try="$ac_compile"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_compile") 2>conftest.err
+  ac_status=$?
+  if test -s conftest.err; then
+    grep -v '^ *+' conftest.err >conftest.er1
+    cat conftest.er1 >&5
+    mv -f conftest.er1 conftest.err
+  fi
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; } && {
+	 test -z "$ac_c_werror_flag" ||
+	 test ! -s conftest.err
+       } && test -s conftest.$ac_objext; then :
+  ac_retval=0
+else
+  $as_echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+	ac_retval=1
+fi
+  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  as_fn_set_status $ac_retval
+
+} @%:@ ac_fn_c_try_compile
+
+@%:@ ac_fn_c_try_link LINENO
+@%:@ -----------------------
+@%:@ Try to link conftest.@S|@ac_ext, and return whether this succeeded.
+ac_fn_c_try_link ()
+{
+  as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
+  rm -f conftest.$ac_objext conftest$ac_exeext
+  if { { ac_try="$ac_link"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_link") 2>conftest.err
+  ac_status=$?
+  if test -s conftest.err; then
+    grep -v '^ *+' conftest.err >conftest.er1
+    cat conftest.er1 >&5
+    mv -f conftest.er1 conftest.err
+  fi
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; } && {
+	 test -z "$ac_c_werror_flag" ||
+	 test ! -s conftest.err
+       } && test -s conftest$ac_exeext && {
+	 test "$cross_compiling" = yes ||
+	 test -x conftest$ac_exeext
+       }; then :
+  ac_retval=0
+else
+  $as_echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+	ac_retval=1
+fi
+  # Delete the IPA/IPO (Inter Procedural Analysis/Optimization) information
+  # created by the PGI compiler (conftest_ipa8_conftest.oo), as it would
+  # interfere with the next link command; also delete a directory that is
+  # left behind by Apple's compiler.  We do this before executing the actions.
+  rm -rf conftest.dSYM conftest_ipa8_conftest.oo
+  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  as_fn_set_status $ac_retval
+
+} @%:@ ac_fn_c_try_link
 cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by lustrec $as_me 1.1-Unversioned directory, which was
+It was created by lustrec $as_me 1.3-      55, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -1679,12 +1788,14 @@ ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $
 ac_compiler_gnu=$ac_cv_c_compiler_gnu
 
 
+VERSION_CODENAME="Xia/Zhong-Kang-dev"
 
+# Next release will be
+#AC_INIT([lustrec], [1.3], [ploc@garoche.net])
+#AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang")
 
-
-$as_echo "@%:@define SVN_REVISION \"Unversioned directory\"" >>confdefs.h
-
-
+#AC_DEFINE(SVN_REVISION, "svnversion", [SVN Revision])
+#AC_SUBST(SVN_REVISION)
 
 
 
@@ -1709,6 +1820,8 @@ fi
 
 
 
+SRC_PATH=/Users/Teme/Documents/GitHub/lustrec
+
 
 # Extract the first word of "ocamlc", so it can be a program name with args.
 set dummy ocamlc; ac_word=$2
@@ -1756,8 +1869,8 @@ $as_echo_n "checking OCaml version... " >&6; }
 ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \  -f 1 | rev`
 major=`echo $ocamlc_version | cut -d . -f 1`
 minor=`echo $ocamlc_version | cut -d . -f 2`
-if (test "$major" -lt 3 -a "$minor" -lt 11 ); then
-  as_fn_error $? "Ocaml version must be at least 3.11. You have version $ocamlc_version" "$LINENO" 5
+if (test "$major" -lt 4 -a "$minor" -lt 0 ); then
+  as_fn_error $? "Ocaml version must be at least 4.0. You have version $ocamlc_version" "$LINENO" 5
 fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: valid ocaml version detected: $ocamlc_version" >&5
 $as_echo "valid ocaml version detected: $ocamlc_version" >&6; }
@@ -1812,13 +1925,893 @@ fi
 $as_echo_n "checking ocamlgraph library... " >&6; }
    ocamlgraph_lib=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 -o "graph.cmxa"`
    if (test "x$ocamlgraph_lib" = xgraph.cmxa ); then
-	ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa  | grep -m 1 "graph.cmxa"`
+	ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 "graph.cmxa"`
       { $as_echo "$as_me:${as_lineno-$LINENO}: result: library detected: $ocamlgraph_lib_full " >&5
 $as_echo "library detected: $ocamlgraph_lib_full " >&6; }
    else
       as_fn_error $? "ocamlgraph library not installed in $OCAMLGRAPH_PATH" "$LINENO" 5
    fi
 
+ac_ext=c
+ac_cpp='$CPP $CPPFLAGS'
+ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
+ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
+ac_compiler_gnu=$ac_cv_c_compiler_gnu
+if test -n "$ac_tool_prefix"; then
+  # Extract the first word of "${ac_tool_prefix}gcc", so it can be a program name with args.
+set dummy ${ac_tool_prefix}gcc; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_CC+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$CC"; then
+  ac_cv_prog_CC="$CC" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    ac_cv_prog_CC="${ac_tool_prefix}gcc"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+fi
+fi
+CC=$ac_cv_prog_CC
+if test -n "$CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
+$as_echo "$CC" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+fi
+if test -z "$ac_cv_prog_CC"; then
+  ac_ct_CC=$CC
+  # Extract the first word of "gcc", so it can be a program name with args.
+set dummy gcc; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_ac_ct_CC+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$ac_ct_CC"; then
+  ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    ac_cv_prog_ac_ct_CC="gcc"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+fi
+fi
+ac_ct_CC=$ac_cv_prog_ac_ct_CC
+if test -n "$ac_ct_CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5
+$as_echo "$ac_ct_CC" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+  if test "x$ac_ct_CC" = x; then
+    CC=""
+  else
+    case $cross_compiling:$ac_tool_warned in
+yes:)
+{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
+$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
+ac_tool_warned=yes ;;
+esac
+    CC=$ac_ct_CC
+  fi
+else
+  CC="$ac_cv_prog_CC"
+fi
+
+if test -z "$CC"; then
+          if test -n "$ac_tool_prefix"; then
+    # Extract the first word of "${ac_tool_prefix}cc", so it can be a program name with args.
+set dummy ${ac_tool_prefix}cc; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_CC+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$CC"; then
+  ac_cv_prog_CC="$CC" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    ac_cv_prog_CC="${ac_tool_prefix}cc"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+fi
+fi
+CC=$ac_cv_prog_CC
+if test -n "$CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
+$as_echo "$CC" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+  fi
+fi
+if test -z "$CC"; then
+  # Extract the first word of "cc", so it can be a program name with args.
+set dummy cc; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_CC+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$CC"; then
+  ac_cv_prog_CC="$CC" # Let the user override the test.
+else
+  ac_prog_rejected=no
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    if test "$as_dir/$ac_word$ac_exec_ext" = "/usr/ucb/cc"; then
+       ac_prog_rejected=yes
+       continue
+     fi
+    ac_cv_prog_CC="cc"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+if test $ac_prog_rejected = yes; then
+  # We found a bogon in the path, so make sure we never use it.
+  set dummy $ac_cv_prog_CC
+  shift
+  if test $@%:@ != 0; then
+    # We chose a different compiler from the bogus one.
+    # However, it has the same basename, so the bogon will be chosen
+    # first if we set CC to just the basename; use the full file name.
+    shift
+    ac_cv_prog_CC="$as_dir/$ac_word${1+' '}$@"
+  fi
+fi
+fi
+fi
+CC=$ac_cv_prog_CC
+if test -n "$CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
+$as_echo "$CC" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+fi
+if test -z "$CC"; then
+  if test -n "$ac_tool_prefix"; then
+  for ac_prog in cl.exe
+  do
+    # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args.
+set dummy $ac_tool_prefix$ac_prog; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_CC+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$CC"; then
+  ac_cv_prog_CC="$CC" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    ac_cv_prog_CC="$ac_tool_prefix$ac_prog"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+fi
+fi
+CC=$ac_cv_prog_CC
+if test -n "$CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
+$as_echo "$CC" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+    test -n "$CC" && break
+  done
+fi
+if test -z "$CC"; then
+  ac_ct_CC=$CC
+  for ac_prog in cl.exe
+do
+  # Extract the first word of "$ac_prog", so it can be a program name with args.
+set dummy $ac_prog; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_ac_ct_CC+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$ac_ct_CC"; then
+  ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    ac_cv_prog_ac_ct_CC="$ac_prog"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+fi
+fi
+ac_ct_CC=$ac_cv_prog_ac_ct_CC
+if test -n "$ac_ct_CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5
+$as_echo "$ac_ct_CC" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+  test -n "$ac_ct_CC" && break
+done
+
+  if test "x$ac_ct_CC" = x; then
+    CC=""
+  else
+    case $cross_compiling:$ac_tool_warned in
+yes:)
+{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
+$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
+ac_tool_warned=yes ;;
+esac
+    CC=$ac_ct_CC
+  fi
+fi
+
+fi
+
+
+test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
+$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
+as_fn_error $? "no acceptable C compiler found in \$PATH
+See \`config.log' for more details" "$LINENO" 5; }
+
+# Provide some information about the compiler.
+$as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5
+set X $ac_compile
+ac_compiler=$2
+for ac_option in --version -v -V -qversion; do
+  { { ac_try="$ac_compiler $ac_option >&5"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_compiler $ac_option >&5") 2>conftest.err
+  ac_status=$?
+  if test -s conftest.err; then
+    sed '10a\
+... rest of stderr output deleted ...
+         10q' conftest.err >conftest.er1
+    cat conftest.er1 >&5
+  fi
+  rm -f conftest.er1 conftest.err
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; }
+done
+
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+ac_clean_files_save=$ac_clean_files
+ac_clean_files="$ac_clean_files a.out a.out.dSYM a.exe b.out"
+# Try to create an executable without -o first, disregard a.out.
+# It will help us diagnose broken compilers, and finding out an intuition
+# of exeext.
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether the C compiler works" >&5
+$as_echo_n "checking whether the C compiler works... " >&6; }
+ac_link_default=`$as_echo "$ac_link" | sed 's/ -o *conftest[^ ]*//'`
+
+# The possible output files:
+ac_files="a.out conftest.exe conftest a.exe a_out.exe b.out conftest.*"
+
+ac_rmfiles=
+for ac_file in $ac_files
+do
+  case $ac_file in
+    *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj ) ;;
+    * ) ac_rmfiles="$ac_rmfiles $ac_file";;
+  esac
+done
+rm -f $ac_rmfiles
+
+if { { ac_try="$ac_link_default"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_link_default") 2>&5
+  ac_status=$?
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; }; then :
+  # Autoconf-2.13 could set the ac_cv_exeext variable to `no'.
+# So ignore a value of `no', otherwise this would lead to `EXEEXT = no'
+# in a Makefile.  We should not override ac_cv_exeext if it was cached,
+# so that the user can short-circuit this test for compilers unknown to
+# Autoconf.
+for ac_file in $ac_files ''
+do
+  test -f "$ac_file" || continue
+  case $ac_file in
+    *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj )
+	;;
+    [ab].out )
+	# We found the default executable, but exeext='' is most
+	# certainly right.
+	break;;
+    *.* )
+	if test "${ac_cv_exeext+set}" = set && test "$ac_cv_exeext" != no;
+	then :; else
+	   ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'`
+	fi
+	# We set ac_cv_exeext here because the later test for it is not
+	# safe: cross compilers may not add the suffix if given an `-o'
+	# argument, so we may need to know it at that point already.
+	# Even if this section looks crufty: it has the advantage of
+	# actually working.
+	break;;
+    * )
+	break;;
+  esac
+done
+test "$ac_cv_exeext" = no && ac_cv_exeext=
+
+else
+  ac_file=''
+fi
+if test -z "$ac_file"; then :
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+$as_echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
+$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
+as_fn_error 77 "C compiler cannot create executables
+See \`config.log' for more details" "$LINENO" 5; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+$as_echo "yes" >&6; }
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler default output file name" >&5
+$as_echo_n "checking for C compiler default output file name... " >&6; }
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_file" >&5
+$as_echo "$ac_file" >&6; }
+ac_exeext=$ac_cv_exeext
+
+rm -f -r a.out a.out.dSYM a.exe conftest$ac_cv_exeext b.out
+ac_clean_files=$ac_clean_files_save
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for suffix of executables" >&5
+$as_echo_n "checking for suffix of executables... " >&6; }
+if { { ac_try="$ac_link"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_link") 2>&5
+  ac_status=$?
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; }; then :
+  # If both `conftest.exe' and `conftest' are `present' (well, observable)
+# catch `conftest.exe'.  For instance with Cygwin, `ls conftest' will
+# work properly (i.e., refer to `conftest.exe'), while it won't with
+# `rm'.
+for ac_file in conftest.exe conftest conftest.*; do
+  test -f "$ac_file" || continue
+  case $ac_file in
+    *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj ) ;;
+    *.* ) ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'`
+	  break;;
+    * ) break;;
+  esac
+done
+else
+  { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
+$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
+as_fn_error $? "cannot compute suffix of executables: cannot compile and link
+See \`config.log' for more details" "$LINENO" 5; }
+fi
+rm -f conftest conftest$ac_cv_exeext
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_exeext" >&5
+$as_echo "$ac_cv_exeext" >&6; }
+
+rm -f conftest.$ac_ext
+EXEEXT=$ac_cv_exeext
+ac_exeext=$EXEEXT
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+@%:@include <stdio.h>
+int
+main ()
+{
+FILE *f = fopen ("conftest.out", "w");
+ return ferror (f) || fclose (f) != 0;
+
+  ;
+  return 0;
+}
+_ACEOF
+ac_clean_files="$ac_clean_files conftest.out"
+# Check that the compiler produces executables we can run.  If not, either
+# the compiler is broken, or we cross compile.
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are cross compiling" >&5
+$as_echo_n "checking whether we are cross compiling... " >&6; }
+if test "$cross_compiling" != yes; then
+  { { ac_try="$ac_link"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_link") 2>&5
+  ac_status=$?
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; }
+  if { ac_try='./conftest$ac_cv_exeext'
+  { { case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; }; }; then
+    cross_compiling=no
+  else
+    if test "$cross_compiling" = maybe; then
+	cross_compiling=yes
+    else
+	{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
+$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
+as_fn_error $? "cannot run C compiled programs.
+If you meant to cross compile, use \`--host'.
+See \`config.log' for more details" "$LINENO" 5; }
+    fi
+  fi
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $cross_compiling" >&5
+$as_echo "$cross_compiling" >&6; }
+
+rm -f conftest.$ac_ext conftest$ac_cv_exeext conftest.out
+ac_clean_files=$ac_clean_files_save
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for suffix of object files" >&5
+$as_echo_n "checking for suffix of object files... " >&6; }
+if ${ac_cv_objext+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+rm -f conftest.o conftest.obj
+if { { ac_try="$ac_compile"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_compile") 2>&5
+  ac_status=$?
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; }; then :
+  for ac_file in conftest.o conftest.obj conftest.*; do
+  test -f "$ac_file" || continue;
+  case $ac_file in
+    *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM ) ;;
+    *) ac_cv_objext=`expr "$ac_file" : '.*\.\(.*\)'`
+       break;;
+  esac
+done
+else
+  $as_echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
+$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
+as_fn_error $? "cannot compute suffix of object files: cannot compile
+See \`config.log' for more details" "$LINENO" 5; }
+fi
+rm -f conftest.$ac_cv_objext conftest.$ac_ext
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_objext" >&5
+$as_echo "$ac_cv_objext" >&6; }
+OBJEXT=$ac_cv_objext
+ac_objext=$OBJEXT
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5
+$as_echo_n "checking whether we are using the GNU C compiler... " >&6; }
+if ${ac_cv_c_compiler_gnu+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+#ifndef __GNUC__
+       choke me
+#endif
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+  ac_compiler_gnu=yes
+else
+  ac_compiler_gnu=no
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+ac_cv_c_compiler_gnu=$ac_compiler_gnu
+
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_c_compiler_gnu" >&5
+$as_echo "$ac_cv_c_compiler_gnu" >&6; }
+if test $ac_compiler_gnu = yes; then
+  GCC=yes
+else
+  GCC=
+fi
+ac_test_CFLAGS=${CFLAGS+set}
+ac_save_CFLAGS=$CFLAGS
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5
+$as_echo_n "checking whether $CC accepts -g... " >&6; }
+if ${ac_cv_prog_cc_g+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_save_c_werror_flag=$ac_c_werror_flag
+   ac_c_werror_flag=yes
+   ac_cv_prog_cc_g=no
+   CFLAGS="-g"
+   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+  ac_cv_prog_cc_g=yes
+else
+  CFLAGS=""
+      cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+  
+else
+  ac_c_werror_flag=$ac_save_c_werror_flag
+	 CFLAGS="-g"
+	 cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+  ac_cv_prog_cc_g=yes
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+   ac_c_werror_flag=$ac_save_c_werror_flag
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_g" >&5
+$as_echo "$ac_cv_prog_cc_g" >&6; }
+if test "$ac_test_CFLAGS" = set; then
+  CFLAGS=$ac_save_CFLAGS
+elif test $ac_cv_prog_cc_g = yes; then
+  if test "$GCC" = yes; then
+    CFLAGS="-g -O2"
+  else
+    CFLAGS="-g"
+  fi
+else
+  if test "$GCC" = yes; then
+    CFLAGS="-O2"
+  else
+    CFLAGS=
+  fi
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5
+$as_echo_n "checking for $CC option to accept ISO C89... " >&6; }
+if ${ac_cv_prog_cc_c89+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_cv_prog_cc_c89=no
+ac_save_CC=$CC
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+#include <stdarg.h>
+#include <stdio.h>
+struct stat;
+/* Most of the following tests are stolen from RCS 5.7's src/conf.sh.  */
+struct buf { int x; };
+FILE * (*rcsopen) (struct buf *, struct stat *, int);
+static char *e (p, i)
+     char **p;
+     int i;
+{
+  return p[i];
+}
+static char *f (char * (*g) (char **, int), char **p, ...)
+{
+  char *s;
+  va_list v;
+  va_start (v,p);
+  s = g (p, va_arg (v,int));
+  va_end (v);
+  return s;
+}
+
+/* OSF 4.0 Compaq cc is some sort of almost-ANSI by default.  It has
+   function prototypes and stuff, but not '\xHH' hex character constants.
+   These don't provoke an error unfortunately, instead are silently treated
+   as 'x'.  The following induces an error, until -std is added to get
+   proper ANSI mode.  Curiously '\x00'!='x' always comes out true, for an
+   array size at least.  It's necessary to write '\x00'==0 to get something
+   that's true only with -std.  */
+int osf4_cc_array ['\x00' == 0 ? 1 : -1];
+
+/* IBM C 6 for AIX is almost-ANSI by default, but it replaces macro parameters
+   inside strings and character constants.  */
+#define FOO(x) 'x'
+int xlc6_cc_array[FOO(a) == 'x' ? 1 : -1];
+
+int test (int i, double x);
+struct s1 {int (*f) (int a);};
+struct s2 {int (*f) (double a);};
+int pairnames (int, char **, FILE *(*)(struct buf *, struct stat *, int), int, int);
+int argc;
+char **argv;
+int
+main ()
+{
+return f (e, argv, 0) != argv[0]  ||  f (e, argv, 1) != argv[1];
+  ;
+  return 0;
+}
+_ACEOF
+for ac_arg in '' -qlanglvl=extc89 -qlanglvl=ansi -std \
+	-Ae "-Aa -D_HPUX_SOURCE" "-Xc -D__EXTENSIONS__"
+do
+  CC="$ac_save_CC $ac_arg"
+  if ac_fn_c_try_compile "$LINENO"; then :
+  ac_cv_prog_cc_c89=$ac_arg
+fi
+rm -f core conftest.err conftest.$ac_objext
+  test "x$ac_cv_prog_cc_c89" != "xno" && break
+done
+rm -f conftest.$ac_ext
+CC=$ac_save_CC
+
+fi
+# AC_CACHE_VAL
+case "x$ac_cv_prog_cc_c89" in
+  x)
+    { $as_echo "$as_me:${as_lineno-$LINENO}: result: none needed" >&5
+$as_echo "none needed" >&6; } ;;
+  xno)
+    { $as_echo "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5
+$as_echo "unsupported" >&6; } ;;
+  *)
+    CC="$CC $ac_cv_prog_cc_c89"
+    { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c89" >&5
+$as_echo "$ac_cv_prog_cc_c89" >&6; } ;;
+esac
+if test "x$ac_cv_prog_cc_c89" != xno; then :
+  
+fi
+
+ac_ext=c
+ac_cpp='$CPP $CPPFLAGS'
+ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
+ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
+ac_compiler_gnu=$ac_cv_c_compiler_gnu
+
+
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for __gmpz_init in -lgmp" >&5
+$as_echo_n "checking for __gmpz_init in -lgmp... " >&6; }
+if ${ac_cv_lib_gmp___gmpz_init+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_check_lib_save_LIBS=$LIBS
+LIBS="-lgmp  $LIBS"
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+/* Override any GCC internal prototype to avoid an error.
+   Use char because int might match the return type of a GCC
+   builtin and then its argument prototype would still apply.  */
+#ifdef __cplusplus
+extern "C"
+#endif
+char __gmpz_init ();
+int
+main ()
+{
+return __gmpz_init ();
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_link "$LINENO"; then :
+  ac_cv_lib_gmp___gmpz_init=yes
+else
+  ac_cv_lib_gmp___gmpz_init=no
+fi
+rm -f core conftest.err conftest.$ac_objext \
+    conftest$ac_exeext conftest.$ac_ext
+LIBS=$ac_check_lib_save_LIBS
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_gmp___gmpz_init" >&5
+$as_echo "$ac_cv_lib_gmp___gmpz_init" >&6; }
+if test "x$ac_cv_lib_gmp___gmpz_init" = xyes; then :
+  gmp=yes
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: GNU MP not found" >&5
+$as_echo "GNU MP not found" >&6; }
+      gmp=no
+fi
+
+
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for mpfr_add in -lmpfr" >&5
+$as_echo_n "checking for mpfr_add in -lmpfr... " >&6; }
+if ${ac_cv_lib_mpfr_mpfr_add+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_check_lib_save_LIBS=$LIBS
+LIBS="-lmpfr  $LIBS"
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+/* Override any GCC internal prototype to avoid an error.
+   Use char because int might match the return type of a GCC
+   builtin and then its argument prototype would still apply.  */
+#ifdef __cplusplus
+extern "C"
+#endif
+char mpfr_add ();
+int
+main ()
+{
+return mpfr_add ();
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_link "$LINENO"; then :
+  ac_cv_lib_mpfr_mpfr_add=yes
+else
+  ac_cv_lib_mpfr_mpfr_add=no
+fi
+rm -f core conftest.err conftest.$ac_objext \
+    conftest$ac_exeext conftest.$ac_ext
+LIBS=$ac_check_lib_save_LIBS
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_mpfr_mpfr_add" >&5
+$as_echo "$ac_cv_lib_mpfr_mpfr_add" >&6; }
+if test "x$ac_cv_lib_mpfr_mpfr_add" = xyes; then :
+  mpfr=yes
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: MPFR not found" >&5
+$as_echo "MPFR not found" >&6; }
+mpfr=no
+fi
+
+
 
 # Workaround to solve an issue with ocamlbuild and C libraries.
 # oCFLAGS="$CFLAGS"
@@ -1856,7 +2849,7 @@ _ACEOF
 
 
 # Instanciation
-ac_config_files="$ac_config_files Makefile src/Makefile src/version.ml"
+ac_config_files="$ac_config_files Makefile src/Makefile src/version.ml test/test-compile.sh"
 
 
 cat >confcache <<\_ACEOF
@@ -2401,7 +3394,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by lustrec $as_me 1.1-Unversioned directory, which was
+This file was extended by lustrec $as_me 1.3-      55, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -2454,7 +3447,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-lustrec config.status 1.1-Unversioned directory
+lustrec config.status 1.3-      55
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 
@@ -2567,6 +3560,7 @@ do
     "Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;;
     "src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;;
     "src/version.ml") CONFIG_FILES="$CONFIG_FILES src/version.ml" ;;
+    "test/test-compile.sh") CONFIG_FILES="$CONFIG_FILES test/test-compile.sh" ;;
 
   *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;;
   esac
@@ -3019,3 +4013,27 @@ fi
 
 
 # summary
+{ $as_echo "$as_me:${as_lineno-$LINENO}: ******** Configuration ********" >&5
+$as_echo "$as_me: ******** Configuration ********" >&6;}
+{ $as_echo "$as_me:${as_lineno-$LINENO}: bin path:     $prefix/bin" >&5
+$as_echo "$as_me: bin path:     $prefix/bin" >&6;}
+{ $as_echo "$as_me:${as_lineno-$LINENO}: include path: $prefix/include" >&5
+$as_echo "$as_me: include path: $prefix/include" >&6;}
+{ $as_echo "$as_me:${as_lineno-$LINENO}: ********    Plugins    ********" >&5
+$as_echo "$as_me: ********    Plugins    ********" >&6;}
+
+  if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
+       { $as_echo "$as_me:${as_lineno-$LINENO}: -mpfr option enable" >&5
+$as_echo "$as_me: -mpfr option enable" >&6;}
+
+   else 
+       { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: MPFR option cannot be activated. Requires GMP and MPFR libs" >&5
+$as_echo "$as_me: WARNING: MPFR option cannot be activated. Requires GMP and MPFR libs" >&2;}
+      
+   fi
+ 
+{ $as_echo "$as_me:${as_lineno-$LINENO}: " >&5
+$as_echo "$as_me: " >&6;}
+{ $as_echo "$as_me:${as_lineno-$LINENO}: ******** Configuration ********" >&5
+$as_echo "$as_me: ******** Configuration ********" >&6;}
+
diff --git a/autom4te.cache/requests b/autom4te.cache/requests
index 25878240f0b628c332c25d8eaf18f8d7595e2172..d37ebb6376a0f623c38614e0545dc60521397428 100644
--- a/autom4te.cache/requests
+++ b/autom4te.cache/requests
@@ -14,63 +14,63 @@
                         'configure.ac'
                       ],
                       {
-                        'm4_pattern_allow' => 1,
-                        'AC_CANONICAL_SYSTEM' => 1,
-                        'AM_PROG_F77_C_O' => 1,
-                        'AC_FC_PP_DEFINE' => 1,
-                        'AM_INIT_AUTOMAKE' => 1,
-                        'LT_CONFIG_LTDL_DIR' => 1,
-                        'AC_LIBSOURCE' => 1,
-                        'AM_POT_TOOLS' => 1,
-                        'AC_CONFIG_LINKS' => 1,
-                        'LT_INIT' => 1,
-                        '_AM_COND_IF' => 1,
-                        'AM_MAKEFILE_INCLUDE' => 1,
-                        '_AM_COND_ELSE' => 1,
-                        'AC_CONFIG_SUBDIRS' => 1,
-                        'AC_SUBST' => 1,
-                        'AC_DEFINE_TRACE_LITERAL' => 1,
-                        'm4_include' => 1,
-                        'm4_pattern_forbid' => 1,
-                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
                         '_AM_MAKEFILE_INCLUDE' => 1,
-                        'AM_PROG_AR' => 1,
-                        'LT_SUPPORTED_TAG' => 1,
-                        'AC_CONFIG_AUX_DIR' => 1,
-                        'AC_CONFIG_LIBOBJ_DIR' => 1,
-                        'AC_PROG_LIBTOOL' => 1,
-                        'AC_FC_PP_SRCEXT' => 1,
-                        'AC_CANONICAL_BUILD' => 1,
-                        'AM_SILENT_RULES' => 1,
+                        'AC_CANONICAL_SYSTEM' => 1,
+                        'AC_INIT' => 1,
                         'AC_CONFIG_FILES' => 1,
                         '_m4_warn' => 1,
-                        'AC_FC_SRCEXT' => 1,
-                        'AC_INIT' => 1,
+                        'm4_sinclude' => 1,
+                        'm4_pattern_forbid' => 1,
+                        '_AM_COND_IF' => 1,
+                        'AH_OUTPUT' => 1,
+                        '_AM_COND_ENDIF' => 1,
+                        'AM_PROG_AR' => 1,
                         'AC_CANONICAL_TARGET' => 1,
-                        'AC_CANONICAL_HOST' => 1,
+                        'LT_SUPPORTED_TAG' => 1,
                         'AC_FC_FREEFORM' => 1,
-                        'AH_OUTPUT' => 1,
+                        'AM_PROG_F77_C_O' => 1,
+                        '_LT_AC_TAGCONFIG' => 1,
                         '_AM_SUBST_NOTMAKE' => 1,
-                        'm4_sinclude' => 1,
-                        'AM_MAINTAINER_MODE' => 1,
-                        'sinclude' => 1,
-                        '_AM_COND_ENDIF' => 1,
+                        'AC_SUBST' => 1,
+                        'AM_MAKEFILE_INCLUDE' => 1,
+                        'LT_INIT' => 1,
+                        'AC_FC_PP_DEFINE' => 1,
+                        'AC_PROG_LIBTOOL' => 1,
                         'AM_XGETTEXT_OPTION' => 1,
+                        'AC_DEFINE_TRACE_LITERAL' => 1,
                         'AC_SUBST_TRACE' => 1,
-                        '_LT_AC_TAGCONFIG' => 1,
-                        'AM_PROG_CXX_C_O' => 1,
-                        'include' => 1,
-                        'AM_GNU_GETTEXT' => 1,
                         'AC_CONFIG_HEADERS' => 1,
+                        'sinclude' => 1,
+                        'AC_CONFIG_LIBOBJ_DIR' => 1,
+                        'AC_LIBSOURCE' => 1,
+                        'AM_POT_TOOLS' => 1,
+                        'AM_GNU_GETTEXT' => 1,
+                        'AM_SILENT_RULES' => 1,
+                        'm4_include' => 1,
+                        'AM_PROG_CC_C_O' => 1,
+                        'AC_CANONICAL_HOST' => 1,
+                        'include' => 1,
+                        'AM_INIT_AUTOMAKE' => 1,
+                        'AM_AUTOMAKE_VERSION' => 1,
+                        'AM_PATH_GUILE' => 1,
+                        'AC_REQUIRE_AUX_FILE' => 1,
+                        'AM_ENABLE_MULTILIB' => 1,
+                        'AC_CANONICAL_BUILD' => 1,
                         'AM_NLS' => 1,
+                        'AC_FC_PP_SRCEXT' => 1,
+                        'AC_CONFIG_LINKS' => 1,
+                        'AC_CONFIG_SUBDIRS' => 1,
+                        'AC_FC_SRCEXT' => 1,
+                        'AM_PROG_CXX_C_O' => 1,
+                        'AM_PROG_MOC' => 1,
+                        'm4_pattern_allow' => 1,
                         'AM_CONDITIONAL' => 1,
                         'AM_PROG_FC_C_O' => 1,
-                        'AC_REQUIRE_AUX_FILE' => 1,
-                        'AM_PROG_MOC' => 1,
-                        'AM_ENABLE_MULTILIB' => 1,
-                        'AM_AUTOMAKE_VERSION' => 1,
-                        'AM_PROG_CC_C_O' => 1,
-                        'AM_PATH_GUILE' => 1
+                        'LT_CONFIG_LTDL_DIR' => 1,
+                        'AM_MAINTAINER_MODE' => 1,
+                        '_AM_COND_ELSE' => 1,
+                        'AC_CONFIG_AUX_DIR' => 1,
+                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1
                       }
                     ], 'Autom4te::Request' )
            );
diff --git a/autom4te.cache/traces.0 b/autom4te.cache/traces.0
index e25ec562112f459da30683a9377667b1d9e612c9..f020f889f204343c740b92cf2e568a8eb4f804a6 100644
--- a/autom4te.cache/traces.0
+++ b/autom4te.cache/traces.0
@@ -152,7 +152,7 @@ m4trace:configure.ac:4: -1- m4_pattern_allow([^VERSION_CODENAME$])
 m4trace:configure.ac:28: -1- AC_SUBST([OCAMLGRAPH_PATH])
 m4trace:configure.ac:28: -1- AC_SUBST_TRACE([OCAMLGRAPH_PATH])
 m4trace:configure.ac:28: -1- m4_pattern_allow([^OCAMLGRAPH_PATH$])
-m4trace:configure.ac:30: -1- AC_SUBST([SRC_PATH], [/Users/Teme/Documents/GitHub/onera_lustrec])
+m4trace:configure.ac:30: -1- AC_SUBST([SRC_PATH], [/Users/Teme/Documents/GitHub/lustrec])
 m4trace:configure.ac:30: -1- AC_SUBST_TRACE([SRC_PATH])
 m4trace:configure.ac:30: -1- m4_pattern_allow([^SRC_PATH$])
 m4trace:configure.ac:32: -1- AC_SUBST([OCAMLC])
@@ -202,24 +202,23 @@ m4trace:configure.ac:99: -1- AC_SUBST_TRACE([abs_datadir])
 m4trace:configure.ac:99: -1- m4_pattern_allow([^abs_datadir$])
 m4trace:configure.ac:99: -1- AC_DEFINE_TRACE_LITERAL([abs_datadir])
 m4trace:configure.ac:99: -1- m4_pattern_allow([^abs_datadir$])
-m4trace:configure.ac:107: -1- AC_CONFIG_FILES([Makefile
+m4trace:configure.ac:106: -1- AC_CONFIG_FILES([Makefile
 		 src/Makefile
-                 src/myocamlbuild.ml
 		 src/version.ml
 		 test/test-compile.sh
 		 ])
-m4trace:configure.ac:109: -1- AC_SUBST([LIB@&t@OBJS], [$ac_libobjs])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([LIB@&t@OBJS])
-m4trace:configure.ac:109: -1- m4_pattern_allow([^LIB@&t@OBJS$])
-m4trace:configure.ac:109: -1- AC_SUBST([LTLIBOBJS], [$ac_ltlibobjs])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([LTLIBOBJS])
-m4trace:configure.ac:109: -1- m4_pattern_allow([^LTLIBOBJS$])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([top_builddir])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([top_build_prefix])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([srcdir])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_srcdir])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([top_srcdir])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_top_srcdir])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([builddir])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_builddir])
-m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_top_builddir])
+m4trace:configure.ac:108: -1- AC_SUBST([LIB@&t@OBJS], [$ac_libobjs])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([LIB@&t@OBJS])
+m4trace:configure.ac:108: -1- m4_pattern_allow([^LIB@&t@OBJS$])
+m4trace:configure.ac:108: -1- AC_SUBST([LTLIBOBJS], [$ac_ltlibobjs])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([LTLIBOBJS])
+m4trace:configure.ac:108: -1- m4_pattern_allow([^LTLIBOBJS$])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([top_builddir])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([top_build_prefix])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([srcdir])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_srcdir])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([top_srcdir])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_top_srcdir])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([builddir])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_builddir])
+m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_top_builddir])
diff --git a/include/math.smt2 b/include/math.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..10bea00ef35867926f6f2c463a1f2bdcf20d87d6
--- /dev/null
+++ b/include/math.smt2
@@ -0,0 +1,6 @@
+(declare-rel  cbrt (Real Real))
+(declare-rel  ceil (Real Real))
+(declare-rel  erf (Real Real))
+(declare-rel  fabs (Real Real))
+(declare-rel  pow (Real Real Real))
+(declare-rel  sqrt (Real Real))
diff --git a/src/backends/Horn/horn_backend_common.ml b/src/backends/Horn/horn_backend_common.ml
index 801a5eb714d1191030720015bb3b9ab690bee953..c40d10ee9caac15bb12b0a6aa9be0a72700d4945 100644
--- a/src/backends/Horn/horn_backend_common.ml
+++ b/src/backends/Horn/horn_backend_common.ml
@@ -69,7 +69,7 @@ let get_machine machines node_name =
 
 let local_memory_vars machines machine =
   rename_machine_list machine.mname.node_id machine.mmemory
-    
+
 let instances_memory_vars ?(without_arrow=false) machines machine =
   let rec aux fst prefix m =
     (
@@ -81,10 +81,10 @@ let instances_memory_vars ?(without_arrow=false) machines machine =
       List.fold_left (fun accu (id, (n, _)) ->
 	let name = node_name n in
 	if without_arrow && name = "_arrow" then
-	  accu 
+	  accu
 	else
 	  let machine_n = get_machine machines name in
-	  ( aux false (concat prefix 
+	  ( aux false (concat prefix
 			 (if fst then id else concat m.mname.node_id id))
 	      machine_n ) @ accu
       ) [] (m.minstances)
@@ -101,16 +101,16 @@ let inout_vars machines m =
 
 let step_vars machines m =
   (inout_vars machines m)
-  @ (rename_current_list (full_memory_vars machines m)) 
+  @ (rename_current_list (full_memory_vars machines m))
   @ (rename_next_list (full_memory_vars machines m))
 
 let step_vars_m_x machines m =
   (inout_vars machines m)
-  @ (rename_mid_list (full_memory_vars machines m)) 
+  @ (rename_mid_list (full_memory_vars machines m))
   @ (rename_next_list (full_memory_vars machines m))
 
 let reset_vars machines m =
-  (rename_current_list (full_memory_vars machines m)) 
+  (rename_current_list (full_memory_vars machines m))
   @ (rename_mid_list (full_memory_vars machines m))
 
 
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index 263f9e5c2d4aa9650111a7730fd1056d43ed5c6f..62b388162e01517293be559811459beee50762ae 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/src/backends/Horn/horn_backend_traces.ml
@@ -39,7 +39,7 @@ let compute_mems machines m =
 
 
 (* We extract the annotation dealing with traceability *)
-let machines_traces machines = 
+let machines_traces machines =
   List.map (fun m ->
     let traces : (ident * expr) list=
       let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
@@ -61,12 +61,12 @@ let machines_traces machines =
     m, traces
 
   ) machines
-  
+
 let memories_old machines m =
   List.map (fun (p, v) ->
     let machine = match p with | [] -> m | (_,m')::_ -> m' in
     let traces = List.assoc machine (machines_traces machines) in
-    if List.mem_assoc v.var_id traces then 
+    if List.mem_assoc v.var_id traces then
       (
 	(* We take the expression associated to variable v in the trace
 	   info *)
@@ -75,20 +75,20 @@ let memories_old machines m =
 	   Printers.pp_expr (List.assoc v.var_id traces); *)
 	p, List.assoc v.var_id traces
       )
-    else 
+    else
       begin
 
 	(* We keep the variable as is: we create an expression v *)
 
 	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v
 	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst
-	   traces); *)	    
+	   traces); *)
 
 	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
       end
 
   ) (compute_mems machines m)
-      
+
 let memories_next  machines m = (* We remove the topest pre in each expression *)
   List.map
     (fun (prefix, ee) ->
@@ -102,15 +102,15 @@ let memories_next  machines m = (* We remove the topest pre in each expression *
       	Printers.pp_expr ee;
       	assert false)
     (memories_old machines m)
-      
+
 
 
 let pp_prefix_rev fmt prefix =
-  Utils.fprintf_list ~sep:"." 
-    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) 
-    fmt 
+  Utils.fprintf_list ~sep:"."
+    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
+    fmt
     (List.rev prefix)
-      
+
 
 let traces_file fmt basename prog machines =
   fprintf fmt "<?xml version=\"1.0\"?>@.";
@@ -120,10 +120,10 @@ let traces_file fmt basename prog machines =
       let pp_var = pp_horn_var m in
       let memories_old = memories_old  machines m in
       let memories_next = memories_next  machines m in
-      
+
       (* fprintf fmt "; Node %s@." m.mname.node_id; *)
       fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;
-      
+
       let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
       let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
       fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
@@ -135,11 +135,11 @@ let traces_file fmt basename prog machines =
 	(Utils.fprintf_list ~sep:" | " pp_var)  output_vars
 	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
 	(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
-      
-      let init_local_vars = 
-	
-	  (rename_next_list (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false)) 
-	
+
+      let init_local_vars =
+	(rename_next_list
+           (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
+
 
       in
       let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in
@@ -160,7 +160,7 @@ let traces_file fmt basename prog machines =
       fprintf fmt "@]@ </Node>";
      )) (List.rev machines);
   fprintf fmt "</Traces>@."
-  
+
 
 (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt
    "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
diff --git a/src/version.ml b/src/version.ml
index eb1860e442e127abf7b053a4c75e8241ff028bbb..e1d4b731beacfebf6c7deb9fec5792bf5b9fe758 100644
--- a/src/version.ml
+++ b/src/version.ml
@@ -1,7 +1,7 @@
 
-let number = "1.1-Unversioned directory"
+let number = "1.3-      55"
 
-let codename ="@VERSION_CODENAME@"
+let codename ="Xia/Zhong-Kang-dev"
 
 let prefix = "/usr/local"
 
diff --git a/test/test-compile.sh b/test/test-compile.sh
index 2ae762778c42a50fb89c5ce410c390540f2ba8a6..f2ee44c325bf4cb324e7ef9c872d87bb5515f9e3 100644
--- a/test/test-compile.sh
+++ b/test/test-compile.sh
@@ -5,21 +5,18 @@ eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
 declare c i w h a v
 declare -a files
 
-SRC_PREFIX=/Users/Teme/Documents/GitHub/onera_lustrec-tests/
+SRC_PREFIX=/Users/Teme/Documents/GitHub/lustrec-tests/
 #SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
 NOW=`date "+%y%m%d%H%M"`
-report=`pwd`/report-1.3-     459-$NOW
+report=`pwd`/report-1.3-      55-$NOW
 LUSTREC=lustrec
 mkdir -p build
 build=`pwd`"/build"
 
 gcc_compile() {
-<<<<<<< HEAD
-=======
     if [ $verbose -gt 1 ]; then
 	echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"
     fi
->>>>>>> onera_master
     gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
     if [ $? -ne 0 ]; then
 	rgcc="INVALID";
@@ -29,12 +26,9 @@ gcc_compile() {
 }
 
 lustrec_compile() {
-<<<<<<< HEAD
-=======
     if [ $verbose -gt 1 ]; then
        echo "$LUSTREC $@"
     fi
->>>>>>> onera_master
     $LUSTREC "$@";
     if [ $? -ne 0 ]; then
         rlustrec="INVALID";
@@ -130,34 +124,6 @@ inline_compile_with_check () {
 	fi
 	dir=${SRC_PREFIX}/`dirname "$file"`
 	pushd $dir > /dev/null
-<<<<<<< HEAD
-    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
-
-    pushd $build > /dev/null
-    gcc_compile "$name"
-	
-    popd > /dev/null
-	# Cheching witness
-    pushd $build > /dev/null
-    lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
-    popd > /dev/null
-    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
-    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
-	rinlining="VALID";
-    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
-	rinlining="ERROR";
-    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
-	rinlining="UNKNOWN";
-    else
-	rinlining="INVALID/TIMEOUT"
-    fi  
-    if [ $verbose -gt 0 ]; then
-	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
-    else
-	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
-    fi
-    popd > /dev/null
-=======
 
 	if [ "$main" != "" ]; then
 	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
@@ -204,7 +170,6 @@ inline_compile_with_check () {
 	else
 	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
 	fi
->>>>>>> onera_master
 done < $file_list
 
 }
@@ -221,15 +186,9 @@ check_prop () {
 	
     # Checking horn backend
     if [ "$main" != "" ]; then
-<<<<<<< HEAD
-	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
-    else
-	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
-=======
 	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
     else
 	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
->>>>>>> onera_master
     fi
 
     # echo "z3 $build/$name".smt2