diff --git a/scripts/frama-c-lustrec.sh b/scripts/frama-c-lustrec.sh
new file mode 100755
index 0000000000000000000000000000000000000000..1577af1453eec82994cb15f60833ac3fddce08a1
--- /dev/null
+++ b/scripts/frama-c-lustrec.sh
@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+
+# simple shell script to launch Frama-C with the right options to
+# prove C files generated by LustreC.
+# look at the usage function for more explanations
+
+# usage function
+usage () {
+    echo "Usage: " $0 " [-h|--help] [-n|--no-strategies] [-t|--timeout T] [frama-c supp. options] file.c"
+    echo "  Launch Frama-C on file.c. Available options:"
+    echo "  - [-h|--help]           | prints this message and exits"
+    echo "  - [-g|--gui]            | use Frama-C GUI"
+    echo "  - [-n|--no-strategies]  | do not use LustreC custom WP strategies"
+    echo "  - [-t|--timeout T]      | set provers timeout to T"
+    echo ""
+    echo "  Frama-C is launched with the following options:"
+    echo "  -wp                                               | use WP plugin"
+    echo "  -wp-model ref,real                                | use ref memory model and ideal floats as reals model"
+    echo "  -wp-prover alt-ergo,z3,cvc4                       | use Alt-Ergo, Z3 and CVC4 SMT solvers"
+    echo "  -wp-par 16                                        | use 16 jobs at most"
+    echo "  -wp-no-warn-memory-model                          | dismiss various memory model related warnings"
+    echo "  -wp-auto LustreC:Transitions,LustreC:MemoryPacks  | use custom proof strategies if -n is not used"
+    echo "  -wp-auto-depth 100                                | set recursive depth limit of custom strategies"
+    echo "  -wp-auto-width 100                                | set maximum number of subgoals for custom strategies"
+    exit 1
+}
+
+# default values
+GUI=
+TIMEOUT=30
+STRATEGIES="-wp-auto LustreC:Transitions,LustreC:MemoryPacks -wp-auto-depth 100 -wp-auto-width 100"
+
+# use getopt to get arguments
+TEMP=$(getopt -o 'ghnt:' --long 'gui,help,no-strategies,timeout:' -n 'frama-c-lustrec.sh' -- "$@")
+
+eval set -- "$TEMP"
+unset TEMP
+
+# main loop to get arguments
+while true; do
+    case "$1" in
+        '-h'|'--help')
+            usage
+        ;;
+        '-g'|'--gui')
+            GUI=-gui
+            shift
+            continue
+        ;;
+        '-n'|'--no-strategies')
+            STRATEGIES=
+            shift
+            continue
+        ;;
+        '-t'|'--timeout')
+            TIMEOUT="$2"
+            shift 2
+            continue
+        ;;
+        *)
+            shift
+            break
+        ;;
+    esac
+done
+
+# launch Frama-C
+frama-c${GUI} -wp \
+       -wp-model ref,real \
+       -wp-prover alt-ergo,z3,cvc4 \
+       -wp-par 16 \
+       -wp-no-warn-memory-model \
+       ${STRATEGIES} \
+       $@