diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml
index 13a58c9..71b8bee 100644
--- a/compiler/main/heptc.ml
+++ b/compiler/main/heptc.ml
@@ -148,6 +148,7 @@ let main () =
         "-fname", Arg.Set full_name, doc_full_name;
         "-itfusion", Arg.Set do_iterator_fusion, doc_itfusion;
         "-strict_ssa", Arg.Unit set_strict_ssa, doc_strict_ssa;
+	"-nosink", Arg.Set nosink, doc_nosink;
         "-memalloc", Arg.Unit do_mem_alloc_and_typing, doc_memalloc;
         "-only-memalloc", Arg.Set do_mem_alloc, doc_memalloc_only;
         "-only-linear", Arg.Set do_linear_typing, doc_linear_only;
diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml
index 8fb77e1..f72adfc 100644
--- a/compiler/minils/sigali/sigalimain.ml
+++ b/compiler/minils/sigali/sigalimain.ml
@@ -402,19 +402,26 @@ let translate_node
       (fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
       (sig_inputs@sig_ctrl) in
   let constraints = constraints @ [Sequal (a_c,Sconst(Ctrue))] in
-  (* Sink state when the guarantee part of the contract becomes false *)
-  (* f_error_state state variable initialized to true; become false
-     the instant after the guarantee part is false *)
-  let error_state_name = f ^ "_error_state" in
-  let sig_states_full = sig_states @ [error_state_name] in
-  let body_sink =
-    [(extend
-        initialisations
-        (Slist[Sequal(Svar(error_state_name),Sconst(Ctrue))]));
-     (extend
-        evolutions
-        (Slist[g_c]))] in
-  let obj = Security(Svar(error_state_name)) in
+  let body_sink, sig_states_full, obj_exp =
+    if !Compiler_options.nosink then
+      ([], sig_states, g_c)
+    else
+      begin
+	(* Sink state when the guarantee part of the contract becomes false *)
+	(* f_error_state state variable initialized to true; become false
+	   the instant after the guarantee part is false *)
+	let error_state_name = f ^ "_error_state" in
+	let sig_states_full = sig_states @ [error_state_name] in
+	let body_sink =
+	  [(extend
+              initialisations
+              (Slist[Sequal(Svar(error_state_name),Sconst(Ctrue))]));
+	   (extend
+              evolutions
+              (Slist[g_c]))] in
+	(body_sink, sig_states_full, Svar(error_state_name))
+      end in
+  let obj = Security(obj_exp) in
   let p = { proc_dep = [];
             proc_name = f;
             proc_inputs = sig_inputs@sig_ctrl;
diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml
index 01fcc27..3109339 100644
--- a/compiler/utilities/global/compiler_options.ml
+++ b/compiler/utilities/global/compiler_options.ml
@@ -85,6 +85,8 @@ let create_object_file = ref false
 
 let boolean = ref false
 
+let nosink = ref false
+
 (* Target languages list for code generation *)
 let target_languages : string list ref = ref []
 
@@ -190,6 +192,7 @@ and doc_target_path =
   "<path>\tGenerated files will be placed in <path>\n\t\t\t(the directory is"
   ^ " cleaned)"
 and doc_boolean = "\t\tTranslate enumerated values towards boolean vectors"
+and doc_nosink = "\t\tSuppress the sink state in sigali equations"
 and doc_deadcode = "\t\tDeadcode removal"
 and doc_nocaus = "\t\tDisable causality analysis"
 and doc_noinit = "\t\tDisable initialization analysis"