diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index e4c436e927be345e896e41c384337e75ec372b45..b56e05647e511df3abb3c24466212c448af4cb85 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -24,9 +24,10 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
 type options =
   { verbose : bool
   ; fragment : CM.fragment_spec
+  ; prop_rate : Reasoner.propagation_rate
   }
 
-let defaultOpts = { verbose = false; fragment = CM.Auto }
+let defaultOpts = { verbose = false; fragment = CM.Auto; prop_rate = Reasoner.Adaptive }
 
 let options =
   [ { Args.long = "verbose"
@@ -61,6 +62,23 @@ let options =
         Args.Required_arg
           ("FRAGMENT", fun s a -> { a with fragment = parse_fragment s })
     }
+  ; { Args.long = "propagationRate"
+    ; Args.short = None
+    ; Args.description = "Rate of Unsat/Sat propagation.\n"
+                         ^ "Possible values are:\n"
+                         ^ "   \"once\": Propagate only when the tableaux is fully expanded\n"
+                         ^ "   \"adaptive\": Automatic mode based on the number of open states\n"
+                         ^ "   INTEGER: Propagate after this many expansion steps"
+    ; Args.argument =
+        let parse_prop_rate s = match s with
+          | "once" -> Reasoner.Once
+          | "adaptive" -> Reasoner.Adaptive
+          | _ -> try Reasoner.Fixed (int_of_string s) with
+                 | Failure _ -> raise (Args.ParseError ("Invalid integer: " ^ s))
+        in
+        Args.Required_arg
+          ("RATE", fun s a -> { a with prop_rate = parse_prop_rate s })
+    }
   ]
 
 let printUsage name =
@@ -126,7 +144,7 @@ let choiceSat opts =
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
           flush stdout;
-          printRes (Reasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox f)
+          printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.prop_rate sorts nomTable tbox f)
         else ()
       done
     with End_of_file -> ()
@@ -151,7 +169,7 @@ let choiceProvable opts =
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
           flush stdout;
-          printRes (Reasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox fneg)
+          printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.prop_rate sorts nomTable tbox fneg)
         else ()
       done
     with End_of_file -> ()
@@ -204,7 +222,7 @@ let choiceGraph opts =
 
   let input = read_line () in
   let (tbox, f) = CoAlgFormula.importQuery input in
-  ignore(Reasoner.isSat opts.fragment sorts nomTable tbox f);
+  ignore(Reasoner.isSat opts.fragment opts.prop_rate sorts nomTable tbox f);
   print_endline (Reasoner.G.graphToDot ())
 
 let choiceVerify opts =
diff --git a/src/coalgcompare/coalgcompare.ml b/src/coalgcompare/coalgcompare.ml
index 73540b2294b7a40aa18bcdea32efea8640e83cca..f91d10832fd83daa3bad9f617fbbc2368340b9e5 100644
--- a/src/coalgcompare/coalgcompare.ml
+++ b/src/coalgcompare/coalgcompare.ml
@@ -125,7 +125,7 @@ let exportALCQuery tbox (_, f) =
 
 
 let solvCoalg sortTable args =
-  G.evaluateFkt (fun (tbox, sf) -> Reasoner.isSat CoAlgMisc.Auto sortTable nomTable tbox sf) args
+  G.evaluateFkt (fun (tbox, sf) -> Reasoner.isSat CoAlgMisc.Auto Reasoner.Adaptive sortTable nomTable tbox sf) args
 
 let solvALC (tbox, sf) =
   let args = exportALCQuery tbox sf in
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index 7c0786de3ffb22fcc4a492aa066466b38a1e634d..990f317a5c89e8c6263db571bc8d2c70808ac010 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -101,7 +101,7 @@ let _ =
     let formula = Sys.argv.(2) in
     let sorts = (FE.sortTableFromString Sys.argv.(1)) in
     let (tbox, f) = CoAlgFormula.importQuery formula in
-    Reasoner.initReasoner CoAlgMisc.Auto sorts nomTable tbox f;
+    Reasoner.initReasoner CoAlgMisc.Auto Reasoner.Adaptive sorts nomTable tbox f;
     let session = {
       Repl.prompt = "> ";
       Repl.bindings = Repl.addHelpBinding [
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 81b2bffbd0804cdcc68c6ba551529ad086bc1ce5..321e200727838c7755cee4694ab5d9018adaf1b3 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -229,7 +229,6 @@ type fragment_spec = Auto | Fragment of fragment
 (** Return the fragment of the mu-calculus that the original formula uses *)
 val getFragment : unit -> fragment
 
-
 type fixpoint_type = MU | NU
 type bound_vars = (fixpoint_type * string * CoAlgFormula.HcFHt.key) list
 
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 24fe15cd59080979f9072fa9422842de2db09ef5..e3a43ded39da4c886cfcb5493acabfc0b6bc44e5 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -21,12 +21,16 @@ exception ReasonerError of string
 
 module type S = sig
 module G : CoolGraph.S
-val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable
+
+type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
+
+val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> propagation_rate
+            -> sortTable
             -> (string -> CoAlgFormula.sort option) ->
             CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
 
 
-val initReasoner : CoAlgMisc.fragment_spec -> sortTable
+val initReasoner : CoAlgMisc.fragment_spec -> propagation_rate -> sortTable
                    -> (string -> CoAlgFormula.sort option) ->
                    CoAlgFormula.sortedFormula list
                    -> CoAlgFormula.sortedFormula -> unit
@@ -269,6 +273,9 @@ let solveGame () =
       end
   in
 
+  if getPropagationRate () == Adaptive then
+    setPropagationCounter (Hashtbl.length seenOpen)
+  else ();
   HashSet.iter applySolution seenOpen
 
 (* let propagateSatMu () = *)
@@ -1216,7 +1223,7 @@ let rec buildGraphLoop () =
   (* if propagating nominals added some more queue members, do all again.. *)
   if queueIsEmpty () then () else buildGraphLoop ()
 
-let initReasoner fragSpec sorts nomTable tbox sf =
+let initReasoner fragSpec propagation_rate sorts nomTable tbox sf =
   sortTable := Array.copy sorts;
   let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in
   let sort = fst sf in
@@ -1225,6 +1232,7 @@ let initReasoner fragSpec sorts nomTable tbox sf =
   graphInit ();
   queueInit ();
   PG_Map.reset ();
+  setPropagationRate propagation_rate;
   let root = insertCore sort bs1 focus in
   graphAddRoot root
 
@@ -1242,6 +1250,7 @@ let reasonerFinished () =
   | Sat  -> true
   | Open -> queueIsEmpty ()
 
+type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
 
 (** A graph-tableau-based decision procedure framework for coalgebraic logics.
     @param verbose An optional switch which determines
@@ -1256,9 +1265,9 @@ let reasonerFinished () =
     @return True if sf is satisfiable wrt tbox, false otherwise.
  *)
 
-let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf =
+let isSat ?(verbose = false) fragSpec propagation_rate sorts nomTable tbox sf =
   let start = if verbose then Unix.gettimeofday () else 0. in
-  initReasoner fragSpec sorts nomTable tbox sf;
+  initReasoner fragSpec propagation_rate sorts nomTable tbox sf;
   let sat =
     try
       buildGraphLoop ();
diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli
index b4081025bef4a085124a18294315556d0543d457..712172e5b0ec80ca9c4cde71b34347142d7b666c 100644
--- a/src/lib/CoAlgReasoner.mli
+++ b/src/lib/CoAlgReasoner.mli
@@ -16,12 +16,20 @@ exception ReasonerError of string
 
 module type S = sig
 module G : CoolGraph.S
-val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable
+
+(** Specifies when cool propagates sat/unsat information. *)
+type propagation_rate = G.propagation_rate =
+  | Once          (** Propagate only when the tableaux is fully expanded *)
+  | Adaptive       (** Automatic mode based on the number of open states *)
+  | Fixed of int   (** Propagate after this many expansion steps *)
+
+val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> propagation_rate
+            -> sortTable
             -> (string -> CoAlgFormula.sort option) ->
             CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
 
 
-val initReasoner : CoAlgMisc.fragment_spec -> sortTable
+val initReasoner : CoAlgMisc.fragment_spec -> propagation_rate -> sortTable
                    -> (string -> CoAlgFormula.sort option) ->
                    CoAlgFormula.sortedFormula list
                    -> CoAlgFormula.sortedFormula -> unit
diff --git a/src/lib/CoolGraph.ml b/src/lib/CoolGraph.ml
index 24382dbfd739a7b5aa54a94b29e1df81850cf7a8..c715f03bba4a1e33dbc64fdb23fa1d30806de4f1 100644
--- a/src/lib/CoolGraph.ml
+++ b/src/lib/CoolGraph.ml
@@ -53,6 +53,10 @@ module type S = sig
   val queueGetElement : unit -> queueElement
   val queuePrettyStatus : unit -> string
 
+  type propagation_rate = Once | Adaptive | Fixed of int
+  val setPropagationRate : propagation_rate -> unit
+  val getPropagationRate : unit -> propagation_rate
+
   val setPropagationCounter : int -> unit
   val doNominalPropagation : unit -> bool
   val doSatPropagation : unit -> bool
@@ -329,19 +333,31 @@ let queueGetElement () =
 
 let doNominalPropagation () = !doPropagation
 
+type propagation_rate = Once | Adaptive | Fixed of int
+
+let prop_rate = ref Once
+
+let setPropagationRate p = prop_rate := p
+
+let getPropagationRate () = !prop_rate
+
 let setPropagationCounter count =
   doPropagationCounter := count
 
-let doSatPropagation () =
-  if !doPropagationCounter == 0
-  then true
-  else begin
-      doPropagationCounter := !doPropagationCounter - 1;
-      false
-    end
-  (* let res = !doPropagation in *)
-  (* doPropagation := false; *)
-  (* res *)
+let doSatPropagation () = match !prop_rate with
+  | Once -> false
+  | Fixed n ->
+     if !doPropagationCounter == 0 then begin
+         doPropagationCounter := n; true
+       end else begin
+         decr doPropagationCounter; false
+       end
+  | Adaptive ->
+     if !doPropagationCounter == 0 then
+         true                   (* the new value has to be set in the reasoner *)
+       else begin
+         decr doPropagationCounter; false
+       end
 
 (*****************************************************************************)
 (*        "Module type" and a specific implementation of the graph           *)
diff --git a/src/lib/CoolGraph.mli b/src/lib/CoolGraph.mli
index 9f3a2b2906c31f574ab3a8331c85f0cd7fb329b6..aae81f2599039c49d2e220d23d0d55f810e0030d 100644
--- a/src/lib/CoolGraph.mli
+++ b/src/lib/CoolGraph.mli
@@ -48,6 +48,10 @@ module type S = sig
   val queueGetElement : unit -> queueElement
   val queuePrettyStatus : unit -> string
 
+  type propagation_rate = Once | Adaptive | Fixed of int
+  val setPropagationRate : propagation_rate -> unit
+  val getPropagationRate : unit -> propagation_rate
+
   val setPropagationCounter : int -> unit
   val doNominalPropagation : unit -> bool
   val doSatPropagation : unit -> bool
diff --git a/src/owl/cool-owl.ml b/src/owl/cool-owl.ml
index 5ea42a06b3059a4fb4ae886706938b61d4e82a6a..b69393fb1a944f126976db73e5c7a26480063f06 100644
--- a/src/owl/cool-owl.ml
+++ b/src/owl/cool-owl.ml
@@ -45,7 +45,7 @@ let consistency () =
         | (_, []) -> raise (Exception "File needs to contain at least one ontology")
     in
     let (sorts,nomTable,axioms) = OWL.to_coalg ontology in
-    let cons = CR.isSat CoAlgMisc.Auto sorts nomTable axioms (0,CF.TRUE) in
+    let cons = CR.isSat CoAlgMisc.Auto CR.Adaptive sorts nomTable axioms (0,CF.TRUE) in
     let cons = if cons then "yes" else "no" in
     let (ontoname, _) = ontology in
     Printf.printf "%s consistent: %s\n" ontoname cons
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index b0b798760f943b3040e53fddedcf0d1349c08fc3..329b4f971ba9231750a9ed6627bfab4f5d07dcb7 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -41,7 +41,7 @@ let runSatCheck (_,logic,input) =
       (* isSat leaks tons of memory. Call it in new process to allow the OS to
          reclaim that memory between calls. *)
       match Unix.fork () with
-      | 0 -> let res = CR.isSat CoAlgMisc.Auto logic nomTable tbox f in
+      | 0 -> let res = CR.isSat CoAlgMisc.Auto CR.Adaptive logic nomTable tbox f in
              if res then exit 0 else exit 1
       | -1 -> raise (CoAlgFormula.CoAlgException "fork() failed")
       | _ -> match Unix.wait () with