diff --git a/preprocessor/.gitignore b/preprocessor/.gitignore
new file mode 100644
index 0000000..f9b5030
--- /dev/null
+++ b/preprocessor/.gitignore
@@ -0,0 +1,3 @@
+preproc_tut
+*.cmi
+*.cmo
diff --git a/preprocessor/Makefile b/preprocessor/Makefile
new file mode 100644
index 0000000..23639d1
--- /dev/null
+++ b/preprocessor/Makefile
@@ -0,0 +1,10 @@
+preproc_tut: preproc_tut.ml
+	ocamlc -o $@ $<
+
+.PHONY: clean veryclean
+
+clean:
+	rm -rf *.cmi *.cmo
+
+veryclean: clean
+	rm -rf preproc_tut
diff --git a/preprocessor/README.md b/preprocessor/README.md
new file mode 100644
index 0000000..9b3f75c
--- /dev/null
+++ b/preprocessor/README.md
@@ -0,0 +1,130 @@
+Overview
+========
+
+This is a small tool for pre-processing the example files in the tutorial.
+
+We would like to ensure that CN's testing infrastructure works well with the
+files in the tutorial, and so it is convenient to add additional annotations
+to the files to support:
+    * mutation testing, to ensure that property based testing is catching
+      mistakes
+    * custom unit test entry points, to ensure that executing specificatoins
+      works as expected.
+
+Both of these could, in principle, be useful to end user of CN, but for
+tutorial purposes it is also conveninet to be able to remove these before
+showing the files for the users.
+
+This preprocessor is intended to help with this task.
+To build it run `make`, and optionally `make clean`.  The result
+should be an executable called `preproc_tut`.
+
+Run `preproc_tut --help` to see a list of available commands.
+
+
+Notation for Mutation Testing
+=============================
+
+The pre-processor is line based.  For mutation testing we use a CPP-like
+if-block, as illustrated by the following example:
+```
+#if !CN_MUTATE_function_containing_the_mutantion_block
+Normal
+code
+path
+#elif MutationName
+Code for
+some
+mutation
+#elif AnotherMutationName
+Some other variant
+#endif
+```
+
+If we run the pre-processer to eliminate mutation testing the result would
+be only:
+
+```
+Normal
+code
+path
+```
+
+
+If we run the pre-processort to generate input for the Etna mutation testing
+tool, we'd get:
+
+```
+//! //
+Normal
+code
+path
+//!! MutationName // //!
+Code for
+some
+mutation
+// //!! AnotherMutationName // //!
+Some other variant
+//
+```
+
+
+Notation for Unit Tests
+=======================
+
+Unit tests are written as CPP conditionals where the condition is
+an identifier that starts with `CN_TEST_` followed by the
+name of the function for the test.  For example:
+
+```
+#if CN_TEST_function_name
+void function_name() {
+  write test here
+}
+#endif
+```
+
+Sometimes we'd also like to indicate that a test is expected to fail. We can
+do this by adding `// fails` on the line declaring the test.
+
+```
+#if CN_TEST_function_name // fails
+void function_name() {
+  write test here
+}
+#endif
+```
+
+This indicates that we expect this test to fail.
+
+
+Scripts
+=======
+
+The directory also contains some scripts which use the preprocessor to run
+the test variations in a file:
+
+  * `run-all CFILE [LOG_FILE]`
+     Test all functions in a file, including unit tests, and mutants.
+     If a LOG_FILE is provided the output of the commands is stored
+     there.  This is useful if tests fails.
+     Mutants are considered to succeed if the corresponding test fails
+     (i.e., they found a bug)
+     Unit tests succeed if the result of testing matches the declarations
+     (see `// fails` above)
+
+  * `config` is a script fragment which defines the locations of external
+     tools
+
+  * `run-cn-test` is a script fragment which defines how we run CN tests
+
+  * `run-unit` can run a single unit test.
+     It just runs the unit test, without checking the expected outcome.
+
+  * `run-mutant` can run a single mutation.
+
+  * `run-prop-tests` test all "normal" functions (i.e., not unit tests or
+    mutants)
+
+
+
diff --git a/preprocessor/config b/preprocessor/config
new file mode 100644
index 0000000..a1e4548
--- /dev/null
+++ b/preprocessor/config
@@ -0,0 +1,11 @@
+
+PREPROC="$SCRIPT_DIR/preproc_tut"
+
+CC="gcc"
+# -P: do not emit line pragmas
+# -CC: do not discard comments
+CPP="$CC -E -P -CC"
+
+CN="cn"
+CN_INSTALL="$OPAM_SWITCH_PREFIX/lib/cn/runtime"
+
diff --git a/preprocessor/example.c b/preprocessor/example.c
new file mode 100644
index 0000000..8aec69a
--- /dev/null
+++ b/preprocessor/example.c
@@ -0,0 +1,39 @@
+// This file show how we envision using the preprocessor.
+
+
+#define S 11111111
+
+int some_other_fun(int x)
+/*@ requires true; ensures return == 0i32; @*/
+{
+  return 0;
+}
+
+int inc(int x)
+/*@ requires 0i32 <= x && x < 10i32; ensures  return < 11i32; @*/
+{
+#if !CN_MUTATE_inc
+  return x + 1;
+#elif X_PLUS_2
+  return x + 2;
+#elif X_PLUS_3
+  return x + 3;
+#endif
+}
+
+
+#if CN_TEST_A // fails
+int A() {
+  inc(S);
+}
+#endif
+
+#if CN_TEST_B
+int B() {
+  inc(5);
+}
+#endif
+
+
+
+
diff --git a/preprocessor/preproc_tut.ml b/preprocessor/preproc_tut.ml
new file mode 100644
index 0000000..3bfd087
--- /dev/null
+++ b/preprocessor/preproc_tut.ml
@@ -0,0 +1,227 @@
+
+let drop_token prefix str =
+  if String.starts_with ~prefix str
+    then
+      let n = String.length prefix in
+      let l = String.length str in
+      Some (String.trim (String.sub str n (l - n)))
+    else None
+
+let rec drop_tokens prefixes str =
+  match prefixes with
+  | [] -> Some str
+  | p :: ps ->
+    match drop_token p str with
+    | Some rest -> drop_tokens ps rest
+    | None -> None
+
+(* Should we start a new mutant block *)
+let start_mutant_block = drop_tokens ["#if"; "!"; "CN_MUTATE_"]
+
+(* Does this line start a mutant *)
+let start_mutant = drop_token "#elif"
+
+(* Does this line start a unit test *)
+let start_unit_test line =
+  match drop_tokens ["#if"; "CN_TEST_"] line with
+  | None -> None
+  | Some name_and_more ->
+    match String.split_on_char '/' name_and_more with
+    | [name; ""; rest] ->
+      let new_name = String.trim name in
+      let fails = String.equal "fails" (String.trim rest) in
+      Some (new_name, fails)
+    | _ -> Some (name_and_more, false)
+
+
+(* Ending for mutant blocks and units tests *)
+let end_named_block = String.starts_with ~prefix:"#endif"
+
+
+
+(* -------------------------------------------------------------------------- *)
+
+
+(* How we are processing the file *)
+type mode =
+  | NoTesting                 (* Remove testing related lines *)
+  | MutationTesting           (* Translate to Etna notation *)
+  | CollectMutants            (* Print only the names of the mutants *)
+  | ExecuteMutant of string   (* Print only this specific mutant *)
+  | CollectUnitTest           (* Print only names of unit tests *)
+  | ExecuteUnitTest of string (* Print only this specific unit test *)
+  | ExecuteAllUnitTests       (* No mutants; all unit tests enabled *)
+
+
+(* The current state of the processor *)
+type state = 
+| TopLevel
+| InMutantOrig of (int * string) (* start line, function name *)
+| InMutant     of (int * string * string) (* start line; function name; mutant name *)
+| InUnitTest   of (int * string) (* start line; test name *)
+
+
+let rec process_input mode start_line state =
+  let mb_line = try Some (read_line()) with End_of_file -> None in
+  match mb_line with
+  | None ->
+    begin
+    let mk_error no msg = failwith (Printf.sprintf "%d: %s" no msg) in
+    match state with
+    | TopLevel          -> ()
+    | InMutantOrig (n,_)-> mk_error n "Untermianted mutant block"
+    | InMutant (n,_,_)  -> mk_error n "Unterminated mutant block"
+    | InUnitTest (n,_)  -> mk_error n "Unterminated unit test"
+    end
+  | Some line ->
+    let new_state =
+      match state with
+  
+      
+      | TopLevel ->
+        begin match start_mutant_block line with
+
+        (* start a mutation test *)
+        | Some fu ->
+          begin match mode with
+          | MutationTesting -> print_endline "//! //"
+          | _               -> ()
+          end;
+          InMutantOrig (start_line,fu) (* next state *)
+        
+        | None ->
+           begin match start_unit_test line with
+   
+             (* start a unit test *)
+             | Some (name,fails) ->
+               begin match mode with
+               | CollectUnitTest ->
+                 Printf.printf "%s/%s\n" name
+                   (if fails then "fails" else "succeeds")
+               | _               -> ()
+               end;
+               InUnitTest (start_line, name) (* next state *)
+   
+             (* ordinary top level line *)
+             | None ->
+               begin match mode with
+               | CollectUnitTest
+               | CollectMutants  -> ()
+               | _               -> print_endline line
+               end;
+               state (* next state *)
+           end
+        end
+
+      | InMutantOrig (ln,fu) ->
+        begin match start_mutant line with
+
+        (* Start a mutant *)
+        | Some name ->
+          begin match mode with
+          | MutationTesting -> Printf.printf "//!! %s // //!\n" name
+          | CollectMutants  -> Printf.printf "%s/%s\n" fu name
+          | _               -> ()
+          end;
+          InMutant (ln,fu,name) (* next state *)
+
+        (* Original part of a mutation block *) 
+        | None ->
+          begin match mode with
+          | CollectUnitTest
+          | CollectMutants 
+          | ExecuteMutant _ -> ()
+          | _               -> print_endline line
+          end;
+          state (* next state *)
+        end
+
+      (* End mutant block *)
+      | InMutant _ when end_named_block line ->
+        begin match mode with
+        | MutationTesting -> print_endline "//"
+        | _               -> ()
+        end;
+        TopLevel (* next state *)
+
+      | InMutant (ln,fu,name) ->
+
+        begin match start_mutant line with
+        (* Next mutatant *)
+        | Some new_name ->
+            begin match mode with
+            | MutationTesting -> Printf.printf "// //!! %s // //!\n" new_name
+            | CollectMutants  -> Printf.printf "%s/%s\n" fu new_name
+            | _               -> ()
+            end;
+            InMutant (ln,fu,new_name) (* next state *)
+
+        (* Line in a mutant *)
+        | None ->
+          begin match mode with
+          | MutationTesting -> print_endline line
+          | ExecuteMutant mu when String.equal mu name -> print_endline line
+          | _ -> ()
+          end;
+          state (* next state *)
+        end
+
+      (* End unit test *)
+      | InUnitTest (ln,name) when end_named_block line ->
+        TopLevel (* next state *)
+
+      (* Line in a unit test *)  
+      | InUnitTest (ln,name) ->
+        begin match mode with
+        | ExecuteAllUnitTests                        -> print_endline line
+        | ExecuteUnitTest t when String.equal name t -> print_endline line
+        | _ -> ()
+        end;
+        InUnitTest (ln,name) (* next state *)
+
+    in process_input mode (start_line + 1) new_state
+
+
+
+let command = ref (None : mode option)
+
+let set_command cmd () =
+  match !command with
+  | None -> command := Some cmd
+  | Some _ -> raise (Arg.Bad "Conflicting command flags")
+
+let do_command str =
+  raise (Arg.Bad (Printf.sprintf "Unexpected argument: %s" str))
+
+let usage = "USAGE:"
+
+let options =
+  Arg.align
+  [ ("--no-test", Arg.Unit (set_command NoTesting),
+    "\tRemove all annotations related to testing");
+
+    ("--etna", Arg.Unit (set_command MutationTesting),
+    "\tEmit mutation tests in CN Etna notation");
+
+    ("--list-mutants", Arg.Unit (set_command CollectMutants),
+    "\tShow the names of the mutants in the input");
+
+    ("--show-mutant", Arg.String (fun name -> set_command (ExecuteMutant name) ()),
+    "NAME\tShow mutant with the given name");
+
+    ("--list-unit", Arg.Unit (set_command CollectUnitTest),
+    "\tShow unit test names and expected outcome");
+
+    ("--show-unit", Arg.String (fun name -> set_command (ExecuteUnitTest name) ()),
+    "NAME\tExecute unit test with the given name");
+
+    ("--show-all-unit", Arg.Unit (set_command ExecuteAllUnitTests),
+    "\tExecute all unit tests without mutations");
+
+  ]
+
+let () =
+  Arg.parse options do_command usage;
+  match !command with
+  | Some mode -> process_input mode 1 TopLevel
+  | None      -> Arg.usage options usage
diff --git a/preprocessor/run-all b/preprocessor/run-all
new file mode 100755
index 0000000..09ee4a0
--- /dev/null
+++ b/preprocessor/run-all
@@ -0,0 +1,86 @@
+#!/bin/bash
+# Run all tests and variations in a C file
+
+LOG_FILE=/dev/null
+
+function usage() {
+  echo "USAGE: $0 CFILE [LOG_FILE]"
+  echo "  Run all tests and variations in single C file."
+  exit 1
+}
+
+if (($# > 2)) || (($# < 1)); then
+  usage
+fi
+
+FILE=$1
+shift
+if (($# > 0)); then
+  LOG_FILE=$1
+fi
+
+echo "$FILE"
+SCRIPT_DIR=$(dirname "$0")
+source "$SCRIPT_DIR/config"
+
+function log_section() {
+  echo "+------------------------------------------------------" >> "$LOG_FILE"
+  echo "| $1" >> "$LOG_FILE"
+  echo "+------------------------------------------------------" >> "$LOG_FILE"
+}
+
+function start_test() {
+  echo -n "  $1"
+  log_section "$1"
+}
+
+FAILURE_COUNT=0
+
+function success() {
+  echo -e "[\033[1;92mOK\033[0m]"
+}
+
+function failure() {
+  echo -e "[\033[1;91mFAIL\033[0m]"
+  FAILURE_COUNT=$(($FAILURE_COUNT + 1))
+}
+
+function end_test() {
+  if [ "$1" == "0" ]; then
+    $2
+  else
+    $3
+  fi
+}
+
+# Testing start from here
+
+
+echo -n "" > "$LOG_FILE"
+log_section "Test start $(date)"
+
+for UNIT in $("$PREPROC" --list-unit < "$FILE"); do
+  TEST=$(dirname "$UNIT")
+  EXPECT=$(basename "$UNIT")
+  start_test "Unit test $TEST: "
+  "$SCRIPT_DIR/run-unit" "$FILE" "$TEST" >> "$LOG_FILE"
+  RESULT=$?
+  if [[ "$EXPECT" == "succeeds" ]]
+    then end_test $RESULT success failure
+    else end_test $RESULT failure success
+  fi
+done
+
+start_test "Checking functions:"
+"$SCRIPT_DIR/run-prop-tests" "$FILE" >> "$LOG_FILE"
+end_test $? success failure
+
+for MUTANT in $("$PREPROC" --list-mutants < "$FILE"); do
+  start_test "Mutant $MUTANT: "
+  "$SCRIPT_DIR/run-mutant" "$FILE" "$MUTANT" >> "$LOG_FILE"
+  end_test $? failure success
+done
+
+exit $FAILURE_COUNT
+
+
diff --git a/preprocessor/run-cn-test b/preprocessor/run-cn-test
new file mode 100644
index 0000000..75cebf0
--- /dev/null
+++ b/preprocessor/run-cn-test
@@ -0,0 +1,16 @@
+# Script fragment for runnin CN tests
+
+source "$SCRIPT_DIR/config"
+
+OUT_DIR=$(mktemp -d /tmp/cn-test-XXXXXX)
+trap 'rm -rf "$OUT_DIR"' EXIT
+
+"$PREPROC" $PREPROC_FLAGS <"$CFILE" >"$OUT_DIR/test-file.c"
+
+pushd "$OUT_DIR" > /dev/null || exit 2
+$CPP "test-file.c" > "test-file.i"
+mv "test-file.i" "test-file.c"
+"$CN" test "test-file.c" --progress-level=0 --output-dir=./run --seed=0 $CN_TEST_FLAGS
+RESULT=$?
+popd > /dev/null || exit 2
+exit $RESULT
\ No newline at end of file
diff --git a/preprocessor/run-mutant b/preprocessor/run-mutant
new file mode 100755
index 0000000..036ca9a
--- /dev/null
+++ b/preprocessor/run-mutant
@@ -0,0 +1,18 @@
+#!/bin/bash
+# Do property based testing for a specific mutant
+#################################################
+
+if [ $# -ne 2 ]; then
+  echo "USAGE: $0 CFILE FUN_QUALIFIED_MUTANT_NAME"
+  echo "  Run a single mutant in the given C file."
+  exit 1
+fi
+
+SCRIPT_DIR=$(dirname "$0")
+CFILE=$1
+FUN=$(dirname "$2")
+UNIT_TEST=$(basename "$2")
+PREPROC_FLAGS="--show-mutant $UNIT_TEST"
+CN_TEST_FLAGS="--only=$FUN"
+source "$SCRIPT_DIR/run-cn-test"
+
diff --git a/preprocessor/run-prop-tests b/preprocessor/run-prop-tests
new file mode 100755
index 0000000..c1c71cf
--- /dev/null
+++ b/preprocessor/run-prop-tests
@@ -0,0 +1,17 @@
+#!/bin/bash
+# Do property based testing for a non-mutated file
+##################################################
+
+if [ $# -ne 1 ]; then
+  echo "USAGE: $0 CFILE"
+  echo "  Run all property based tests in a given C file."
+  exit 1
+fi
+
+SCRIPT_DIR=$(dirname "$0")
+CFILE=$1
+PREPROC_FLAGS="--no-test"
+CN_TEST_FLAGS=""
+source "$SCRIPT_DIR/run-cn-test"
+
+
diff --git a/preprocessor/run-unit b/preprocessor/run-unit
new file mode 100755
index 0000000..bae4549
--- /dev/null
+++ b/preprocessor/run-unit
@@ -0,0 +1,19 @@
+#!/bin/bash
+# Do property based testing for a specific unit test
+####################################################
+
+if [ $# -ne 2 ]; then
+  echo "USAGE: $0 CFILE TEST"
+  echo "  Run a unit test."
+  exit 1
+fi
+
+SCRIPT_DIR=$(dirname "$0")
+CFILE=$1
+FUN=$2
+PREPROC_FLAGS="--show-unit $FUN"
+CN_TEST_FLAGS="--only=$FUN"
+source "$SCRIPT_DIR/run-cn-test"
+
+
+