diff --git a/Makefile.in b/Makefile.in
index f011d5f1..b0e3454d 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -82,7 +82,11 @@ SRC_MODULES = \
 	cuter_strategy \
 	cuter_bfs_strategy \
 	cuter_metrics \
-	cuter_config
+	cuter_config \
+	cuter_spec_checker \
+	cuter_graphs \
+	cuter_maybe_error_annotation \
+	cuter_type_dependent_functions
 
 UTEST_MODULES = \
 	cuter_tests_lib \
@@ -100,7 +104,11 @@ UTEST_MODULES = \
 	types_and_specs \
 	types_and_specs2 \
 	cuter_metrics_tests \
-	cuter_config_tests
+	cuter_config_tests \
+	cuter_graphs_tests \
+	callgraph_examples \
+	examples_for_spec_conversion \
+	examples_for_spec_conversion_pair
 
 FTEST_MODULES = \
 	bitstr \
diff --git a/cuter b/cuter
index 9a72d699..d369aa64 100755
--- a/cuter
+++ b/cuter
@@ -38,6 +38,7 @@ def main():
   parser.add_argument("-m", "--metrics", action='store_true', help="report collected metrics")
   parser.add_argument("--debug-keep-traces", action='store_true', help="keep execution traces for debugging")
   parser.add_argument("--debug-solver-fsm", action='store_true', help="output debug logs for the solver FSM")
+  parser.add_argument("-ps", "--prune-safe", action='store_true', help="prune safe paths and stop the execution early")
 
   # Parse the arguments
   args = parser.parse_args()
@@ -109,6 +110,8 @@ def main():
     opts.append("debug_keep_traces")
   if args.debug_solver_fsm:
     opts.append("debug_solver_fsm")
+  if args.prune_safe:
+    opts.append("prune_safe")
   strOpts = ",".join(opts)
 
   # Run CutEr
diff --git a/include/cuter_macros.hrl b/include/cuter_macros.hrl
index 8572c4cd..d9af4a12 100644
--- a/include/cuter_macros.hrl
+++ b/include/cuter_macros.hrl
@@ -89,6 +89,8 @@
 -define(NUM_SOLVERS, number_of_solvers).
 %% Sets the number of concurrent concolic execution processes.
 -define(NUM_POLLERS, number_of_pollers).
+%% Prune safe paths.
+-define(PRUNE_SAFE, prune_safe).
 
 -type runtime_options() :: {?Z3_TIMEOUT, pos_integer()} 
                          | ?REPORT_METRICS
@@ -104,6 +106,7 @@
                          | {?NUM_SOLVERS, pos_integer()}
                          | {?NUM_POLLERS, pos_integer()}
                          | {?WORKING_DIR, file:filename()}
+			 | ?PRUNE_SAFE
                          .
 
 %%====================================================================
@@ -156,3 +159,10 @@
 
 %% Empty tag ID
 -define(EMPTY_TAG_ID, 0).
+
+%%====================================================================
+%% Miscellaneous stored values in cuter config
+%%====================================================================
+
+%% Entry point for concolic testing
+-define(ENTRY_POINT, entry_point).
diff --git a/src/cuter.erl b/src/cuter.erl
index 0e07eb8f..95e3a85a 100644
--- a/src/cuter.erl
+++ b/src/cuter.erl
@@ -48,7 +48,7 @@ run(M, F, As, Depth, Options) ->
   Seeds = [{M, F, As, Depth}],
   run(Seeds, Options).
 
--spec run([seed()], options()) -> erroneous_inputs().
+-spec run([seed(),...], options()) -> erroneous_inputs().
 %% Runs CutEr on multiple units.
 run(Seeds, Options) ->
   State = state_from_options_and_seeds(Options, Seeds),
@@ -90,7 +90,8 @@ run_from_file(File, Options) ->
 %% The tasks to run during the app initialization.
 init_tasks() ->
   [fun ensure_exported_entry_points/1,
-   fun compute_callgraph/1].
+   fun compute_callgraph/1,
+   fun annotate_for_possible_errors/1].
 
 -spec init(state()) -> ok | error.
 init(State) ->
@@ -131,10 +132,17 @@ compute_callgraph(State) ->
   Mfas = mfas_from_state(State),
   cuter_codeserver:calculate_callgraph(State#st.codeServer, Mfas).
 
-
 mfas_from_state(State) ->
   [{M, F, length(As)} || {M, F, As, _} <- State#st.seeds].
 
+annotate_for_possible_errors(State) ->
+  case cuter_config:fetch(?PRUNE_SAFE) of
+    {ok, true} ->
+      cuter_codeserver:annotate_for_possible_errors(State#st.codeServer);
+    _ ->
+      ok
+  end.
+
 %% ----------------------------------------------------------------------------
 %% Manage the concolic executions
 %% ----------------------------------------------------------------------------
@@ -146,8 +154,7 @@ start(State) ->
 -spec start([seed()], state()) -> state().
 start([], State) ->
   State;
-start([{M, F, As, Depth}|Seeds], State) ->
-  CodeServer = State#st.codeServer,
+start([{M, F, As, Depth}|Seeds], State) ->  CodeServer = State#st.codeServer,
   Scheduler = State#st.scheduler,
   Errors = start_one(M, F, As, Depth, CodeServer, Scheduler),
   NewErrors = [{{M, F, length(As)}, Errors}|State#st.errors],
@@ -242,7 +249,7 @@ stop(State) ->
 %% Generate the system state
 %% ----------------------------------------------------------------------------
 
--spec state_from_options_and_seeds(options(), [seed()]) -> state().
+-spec state_from_options_and_seeds(options(), [seed(),...]) -> state().
 state_from_options_and_seeds(Options, Seeds) ->
   process_flag(trap_exit, true),
   error_logger:tty(false),  %% disable error_logger
@@ -250,11 +257,11 @@ state_from_options_and_seeds(Options, Seeds) ->
   ok = cuter_metrics:start(),
   ok = define_metrics(),
   enable_debug_config(Options),
-  enable_runtime_config(Options),
+  enable_runtime_config(Options, Seeds),
   ok = cuter_pp:start(),
   CodeServer = cuter_codeserver:start(),
   SchedPid = cuter_scheduler:start(?DEFAULT_DEPTH, CodeServer),
-  #st{ codeServer = CodeServer, scheduler = SchedPid, seeds = Seeds }.
+  #st{codeServer = CodeServer, scheduler = SchedPid, seeds = Seeds}.
 
 define_metrics() ->
   define_distribution_metrics().
@@ -268,8 +275,8 @@ enable_debug_config(Options) ->
   cuter_config:store(?DEBUG_SMT, proplists:get_bool(?DEBUG_SMT, Options)),
   cuter_config:store(?DEBUG_SOLVER_FSM, proplists:get_bool(?DEBUG_SOLVER_FSM, Options)).
 
--spec enable_runtime_config(options()) -> ok.
-enable_runtime_config(Options) ->
+-spec enable_runtime_config(options(), [seed(),...]) -> ok.
+enable_runtime_config(Options, [{M, F, I, _D}|_]) ->
   {ok, CWD} = file:get_cwd(),
   cuter_config:store(?WORKING_DIR,
                      cuter_lib:get_tmp_dir(proplists:get_value(?WORKING_DIR, Options, CWD))),
@@ -287,7 +294,9 @@ enable_runtime_config(Options) ->
   cuter_config:store(?SORTED_ERRORS, proplists:get_bool(?SORTED_ERRORS, Options)),
   cuter_config:store(?WHITELISTED_MFAS, whitelisted_mfas(Options)),
   cuter_config:store(?NUM_SOLVERS, proplists:get_value(?NUM_SOLVERS, Options, ?ONE)),
-  cuter_config:store(?NUM_POLLERS, proplists:get_value(?NUM_POLLERS, Options, ?ONE)).
+  cuter_config:store(?NUM_POLLERS, proplists:get_value(?NUM_POLLERS, Options, ?ONE)),
+  cuter_config:store(?PRUNE_SAFE, proplists:get_bool(?PRUNE_SAFE, Options)),
+  cuter_config:store(?ENTRY_POINT, {M, F, length(I)}).
 
 verbosity_level(Options) ->
   Default = cuter_pp:default_reporting_level(),
diff --git a/src/cuter_cerl.erl b/src/cuter_cerl.erl
index d8f742ec..a99f0fec 100644
--- a/src/cuter_cerl.erl
+++ b/src/cuter_cerl.erl
@@ -12,7 +12,7 @@
          node_types_conditions/0, node_types_conditions_nocomp/0,
          node_types_paths/0, node_types_paths_nocomp/0]).
 %% kfun API.
--export([kfun/2, kfun_code/1, kfun_is_exported/1]).
+-export([kfun/2, kfun_code/1, kfun_is_exported/1, kfun_update_code/2]).
 %% kmodule API.
 -export([kmodule_spec_forms/1, kmodule_record_forms/1, kmodule_type_forms/1, kmodule_exported_types/1, kmodule_name/1, destroy_kmodule/1, kmodule/3, kmodule_kfun/2, kmodule_mfa_spec/2,
   kmodule_specs/1, kmodule_types/1, kmodule_update_kfun/3, kmodule_mfas_with_kfuns/1,
@@ -25,13 +25,12 @@
 
 -include("include/cuter_macros.hrl").
 
--export_type([compile_error/0, cerl_attr_spec/0, cerl_attr_type/0,
+-export_type([compile_error/0, cerl_spec_form/0, cerl_attr_type/0,
 	      cerl_bounded_func/0, cerl_constraint/0, cerl_func/0,
-	      cerl_recdef/0, cerl_record_field/0, cerl_spec/0,
+	      cerl_record_field/0, cerl_spec/0,
 	      cerl_spec_func/0, cerl_type/0, cerl_typedef/0,
 	      cerl_type_record_field/0, node_types/0,
-	      tagID/0, tag/0, tag_generator/0, visited_tags/0,
-	      spec_info/0]).
+	      tagID/0, tag/0, tag_generator/0, visited_tags/0]).
 
 -export_type([extracted_record_form/0, extracted_type_form/0]).
 
@@ -70,17 +69,15 @@
 -type name() :: atom().
 -type fa() :: {name(), arity()}.
 -type cerl_attr_type() :: cerl_recdef() | cerl_typedef().
--type cerl_attr_spec() :: cerl_specdef().
 
--type cerl_recdef() :: {name(), [cerl_record_field()]} % for OTP 19.x
-                     | {{'record', name()}, [cerl_record_field()], []}. % for OTP 18.x or earlier
+-type cerl_recdef() :: {name(), [cerl_record_field()]}.
 -type cerl_record_field() :: cerl_untyped_record_field() | cerl_typed_record_field().
 -type cerl_untyped_record_field() :: {'record_field', lineno(), {'atom', lineno(), name()}}
                                    | {'record_field', lineno(), {'atom', lineno(), name()}, any()}.
 -type cerl_typed_record_field() :: {'typed_record_field', cerl_untyped_record_field(), cerl_type()}.
 -type cerl_typedef() :: {name(), cerl_type(), [cerl_type_var()]}.
 
--type cerl_specdef() :: {fa(), cerl_spec()}.
+-type cerl_spec_form() :: {fa(), cerl_spec()}.
 -type cerl_spec() :: [cerl_spec_func(), ...].
 -type cerl_spec_func() :: cerl_func() | cerl_bounded_func().
 
@@ -273,7 +270,7 @@ is_mfa({M, F, A}) when is_atom(M), is_atom(F), is_integer(A), A >= 0 -> true;
 is_mfa(_Mfa) -> false.
 
 %% Returns the unprocessed specs of a kmodule (as forms).
--spec kmodule_spec_forms(kmodule()) -> [cerl:cerl()].
+-spec kmodule_spec_forms(kmodule()) -> [cerl_spec_form()].
 kmodule_spec_forms(Kmodule) ->
   [{spec_forms, SpecsForms}] = ets:lookup(Kmodule, spec_forms),
   SpecsForms.
@@ -310,6 +307,9 @@ kfun_is_exported(#{is_exported := IsExported}) -> IsExported.
 -spec kfun_code(kfun()) -> code().
 kfun_code(#{code := Code}) -> Code.
 
+-spec kfun_update_code(kfun(), code()) -> kfun().
+kfun_update_code(Fun, Code) -> Fun#{code=>Code}.
+
 %% ===================================================================
 %% Internal functions
 %% ===================================================================
@@ -320,8 +320,8 @@ extract_exports(M, AST) ->
   [mfa_from_var(M, E) || E <- Exports].
 
 extract_exported_types(Mod, Attrs) ->
-  Filtered = [T || {#c_literal{val = export_type}, #c_literal{val = T}} <- Attrs],
-  sets:from_list(lists:append([{Mod, Tname, Tarity} || {Tname, Tarity} <- Filtered])).
+  ExpTypes = lists:append([Ts || {#c_literal{val = export_type}, #c_literal{val = Ts}} <- Attrs]),
+  sets:from_list([{Mod, Tname, Tarity} || {Tname, Tarity} <- ExpTypes]).
 
 -spec process_fundef({cerl:c_var(), code()}, [mfa()], module(), tag_generator()) -> {mfa(), kfun()}.
 process_fundef({FunVar, Def}, Exports, M, TagGen) ->
@@ -375,8 +375,6 @@ get_abstract_code(Mod, Beam) ->
     _ -> throw(cuter_pp:abstract_code_missing(Mod))
   end.
 
--type spec_info() :: cerl_attr_spec().
-
 %% Extracts the record definitions (as forms) from the annotations of a module.
 %% The relevant annotations have the following structure in OTP 19.x and newer:
 %%     {#c_atom{val=record}, #c_literal{val=[{Name, Fields}]}}
diff --git a/src/cuter_codeserver.erl b/src/cuter_codeserver.erl
index d4962a51..17777915 100644
--- a/src/cuter_codeserver.erl
+++ b/src/cuter_codeserver.erl
@@ -10,6 +10,8 @@
          visit_tag/2, calculate_callgraph/2,
          %% Work with module cache
          merge_dumped_cached_modules/2, modules_of_dumped_cache/1,
+	 %% Code annotations
+	 annotate_for_possible_errors/1,
          %% Access logs
          cachedMods_of_logs/1, visitedTags_of_logs/1, tagsAddedNo_of_logs/1,
          unsupportedMfas_of_logs/1, loadedMods_of_logs/1]).
@@ -19,6 +21,8 @@
 %% Counter of branches & Tag generator.
 -export([get_branch_counter/0, init_branch_counter/0, generate_tag/0]).
 
+-export([convert_specs/1]).
+
 -include("include/cuter_macros.hrl").
 
 -export_type([cached_modules/0, codeserver/0, counter/0, logs/0]).
@@ -27,7 +31,7 @@
 -define(BRANCH_COUNTER_PREFIX, '__branch_count').
 
 -type counter() :: non_neg_integer().
--type cached_module_data() :: any().
+-type cached_module_data() :: any().   % XXX: refine
 -type cached_modules() :: dict:dict(module(), cached_module_data()).
 
 -type cache() :: ets:tid().
@@ -46,12 +50,12 @@
 }).
 -type logs() :: #logs{}.
 
-%% Internal type declarations
+%% Internal type declarations.
 -type load_reply() :: {ok, cuter_cerl:kmodule()} | cuter_cerl:compile_error() | {error, (preloaded | cover_compiled | non_existing)}.
 -type spec_reply() :: {ok, cuter_types:erl_spec()} | error.
 -type from() :: {pid(), reference()}.
 
-%% Finding the remote dependencies of a spec.
+%% Remote dependencies of a spec.
 -type remote_type()     :: {cuter:mod(), atom(), byte()}.
 -type module_deps()     :: ordsets:ordset(cuter:mod()).
 -type visited_remotes() :: ordsets:ordset(remote_type()).
@@ -59,7 +63,7 @@
 -type codeserver() :: pid().
 -type codeserver_args() :: #{}.
 
-%% Server's state
+%% Server's state.
 -record(st, {
   %% Acts as a reference table for looking up the ETS table that holds a module's extracted code.
   %% It stores tuples {Module :: module(), ModuleDb :: ets:tid()}.
@@ -137,11 +141,20 @@ get_whitelist(CodeServer) ->
 calculate_callgraph(CodeServer, Mfas) ->
   gen_server:call(CodeServer, {calculate_callgraph, Mfas}).
 
+-spec convert_specs(codeserver()) -> ok.
+convert_specs(CodeServer) ->
+  gen_server:call(CodeServer, convert_specs).
+
 %% Gets the feasible tags.
 -spec get_feasible_tags(codeserver(), cuter_cerl:node_types()) -> cuter_cerl:visited_tags().
 get_feasible_tags(CodeServer, NodeTypes) ->
   gen_server:call(CodeServer, {get_feasible_tags, NodeTypes}).
 
+%% Annotates the code for possible errors.
+-spec annotate_for_possible_errors(codeserver()) -> ok.
+annotate_for_possible_errors(CodeServer) ->
+  gen_server:call(CodeServer, annotate_for_possible_errors).
+
 %% ----------------------------------------------------------------------------
 %% gen_server callbacks (Server Implementation)
 %% ----------------------------------------------------------------------------
@@ -182,6 +195,7 @@ handle_info(_Msg, State) ->
                ; (get_whitelist, from(), state()) -> {reply, cuter_mock:whitelist(), state()}
                ; ({get_feasible_tags, cuter_cerl:node_types()}, from(), state()) -> {reply, cuter_cerl:visited_tags(), state()}
                ; ({calculate_callgraph, [mfa()]}, from(), state()) -> {reply, ok, state()}
+	             ; (annotate_for_possible_errors, from(), state()) -> {reply, ok, state()}
                .
 handle_call({load, M}, _From, State) ->
   {reply, try_load(M, State), State};
@@ -231,7 +245,28 @@ handle_call({calculate_callgraph, Mfas}, _From, State=#st{whitelist = Whitelist}
                 end,
       cuter_callgraph:foreachModule(LoadFn, Callgraph),
       {reply, ok, State#st{callgraph = Callgraph}}
-  end.
+  end;
+handle_call(annotate_for_possible_errors, _From, State=#st{db = Db}) ->
+  Fn = fun({_M, Kmodule}, KfunAcc) ->
+      KfunMappings = cuter_cerl:kmodule_mfas_with_kfuns(Kmodule),
+      TrivialMergeFn = fun(_K, V1, _V2) -> V1 end,
+      dict:merge(TrivialMergeFn, KfunAcc, KfunMappings)
+    end,
+  Fn2 = fun({_M, Kmodule}, Acc) ->
+	    [Kmodule|Acc]
+	end,
+  Kmodules = ets:foldl(Fn2, [], Db),
+  {ok, EntryPoint} = cuter_config:fetch(?ENTRY_POINT),
+  MfasToKfuns = ets:foldl(Fn, dict:new(), Db),
+  MfasToSpecs = cuter_types:specs_as_erl_types(Kmodules),
+  UpdatedKfuns = cuter_maybe_error_annotation:preprocess(EntryPoint, MfasToKfuns, MfasToSpecs),
+  RFn = fun({M, F, A}, Kfun, _Acc) ->
+	   [{_M, Kmodule}] = ets:lookup(Db, M),
+	    cuter_cerl:kmodule_update_kfun(Kmodule, {M, F, A}, Kfun)
+	end,
+  dict:fold(RFn, ok, UpdatedKfuns),
+  {reply, ok, State}.
+
 
 %% gen_server callback : handle_cast/2
 -spec handle_cast(stop, state()) -> {stop, normal, state()} | {noreply, state()}
@@ -254,10 +289,10 @@ handle_cast({visit_tag, Tag}, State=#st{tags = Tags}) ->
 -spec load_all_deps_of_spec(cuter_types:stored_spec_value(), module(), cuter_cerl:kmodule(), state()) -> [cuter:mod()].
 load_all_deps_of_spec(CerlSpec, Module, Kmodule, State) ->
   LocalTypesCache = cuter_cerl:kmodule_types(Kmodule),
-  % Get the remote dependencies of the spec.
+  %% Get the remote dependencies of the spec.
   ToBeVisited = cuter_types:find_remote_deps_of_spec(CerlSpec, LocalTypesCache),
   InitDepMods = ordsets:add_element(Module, ordsets:new()),
-  % Find iteratively the dependencies of the found dependencies.
+  %% Find iteratively the dependencies of the found dependencies.
   case load_all_deps(ToBeVisited, State, ordsets:new(), InitDepMods) of
     error -> [];
     {ok, DepMods} -> DepMods
@@ -285,7 +320,7 @@ load_all_deps([Remote={M, TypeName, Arity}|Rest], State, VisitedRemotes, DepMods
               Deps = cuter_types:find_remote_deps_of_type(Type, LocalTypesCache),
               %% Queue the ones that we haven't encountered yet.
               NewRemotes = [R || R <- Deps,
-                not ordsets:is_element(R, VisitedRemotes1)],
+				 not ordsets:is_element(R, VisitedRemotes1)],
               load_all_deps(NewRemotes ++ Rest, State, VisitedRemotes1, DepMods1)
           end;
         _Msg ->
diff --git a/src/cuter_debug.erl b/src/cuter_debug.erl
index f6ce493c..3e2d3810 100644
--- a/src/cuter_debug.erl
+++ b/src/cuter_debug.erl
@@ -1,16 +1,29 @@
 %% -*- erlang-indent-level: 2 -*-
 %%------------------------------------------------------------------------------
 -module(cuter_debug).
--export([parse_module/2]).
+
+-export([parse_module/2, to_erl_types_specs/1]).
+
+%% This module contains utilities for debugging purposes during the
+%% development of the tool.
 
 %% Prints the AST of a module.
-%% Run as:
-%%   erl -noshell -pa ebin/ -eval "cuter_debug:parse_module(lists, true)" -s init stop
 -spec parse_module(module(), boolean()) -> ok.
 parse_module(M, WithPmatch) ->
-	case cuter_cerl:get_core(M, WithPmatch) of
+  case cuter_cerl:get_core(M, WithPmatch) of
     {error, E} ->
       io:format("ERROR: ~p~n", [E]);
     {ok, AST} ->
       io:format("~p~n", [AST])
   end.
+
+%% Prints the erl_types representation of all specs in a list of modules.
+-spec to_erl_types_specs([module()]) -> ok.
+to_erl_types_specs(Modules) ->
+  Fn = fun(M) -> {ok, AST} = cuter_cerl:get_core(M, false), AST end,
+  Kmodules = [cuter_cerl:kmodule(M, Fn(M), fun () -> ok end) || M <- Modules],
+  Specs = cuter_types:specs_as_erl_types(Kmodules),
+  lists:foreach(fun print_mfa_and_spec/1, dict:to_list(Specs)).
+
+print_mfa_and_spec({MFA, Spec}) ->
+  io:format("~p~n  ~p~n", [MFA, Spec]).
diff --git a/src/cuter_eval.erl b/src/cuter_eval.erl
index 1dfe51db..a754b8ac 100644
--- a/src/cuter_eval.erl
+++ b/src/cuter_eval.erl
@@ -36,6 +36,11 @@
 }).
 -type valuelist() :: #valuelist{}.
 
+%% Runtime options for the evaluator function of the interpreter.
+-type eval_opts() :: #{constraintLogging := boolean(),
+                       isForced := boolean(),
+                       distrustTypeDependent := boolean()}.
+
 %% ----------------------------------------------------------------------------
 %% Types and macros used for storing the information of applying a lambda
 %% that has a symbolic value.
@@ -139,12 +144,15 @@ log_mfa_spec(_, _, _) -> ok.
 %% Concrete/Symbolic Evaluation and Logging of an MFA call
 %% -------------------------------------------------------------------
 -spec eval(eval(), [any()], [any()], calltype(), servers(), file:io_device()) -> result().
-
+eval(A, CAs, SAs, CallType, Servers, Fd) ->
+  DefaultOptions = #{isForced => false, constraintLogging => true, distrustTypeDependent => false},
+  eval(A, CAs, SAs, CallType, Servers, Fd, DefaultOptions).
 %% Handle spawns so that the spawned process will be interpreted
 %% and not directly executed
 
 %% spawn/{1,2,3,4} & spawn_link/{1,2,3,4}
-eval({named, erlang, F}, CAs, SAs, _CallType, Servers, Fd) when F =:= spawn; F =:= spawn_link ->
+-spec eval(eval(), [any()], [any()], calltype(), servers(), file:io_device(), eval_opts()) -> result().
+eval({named, erlang, F}, CAs, SAs, _CallType, Servers, Fd, Options) when F =:= spawn; F =:= spawn_link ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   Rf = erlang:make_ref(),
@@ -183,12 +191,12 @@ eval({named, erlang, F}, CAs, SAs, _CallType, Servers, Fd) when F =:= spawn; F =
     end,
   receive
     {ChildP, registered} ->
-      cuter_log:log_spawn(Fd, ChildP, Rf),
+      conditional_log(fun cuter_log:log_spawn/3, [Fd, ChildP, Rf], Options),
       mk_result(ChildP, ChildP)
   end;
 
 %% spawn_monitor/{1,3}
-eval({named, erlang, spawn_monitor}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({named, erlang, spawn_monitor}, CAs, SAs, _CallType, Servers, Fd, Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   Rf = erlang:make_ref(),
@@ -210,12 +218,12 @@ eval({named, erlang, spawn_monitor}, CAs, SAs, _CallType, Servers, Fd) ->
   {ChildP, _ChildRef} = CC = erlang:spawn_monitor(Child),
   receive
     {ChildP, registered} ->
-      cuter_log:log_spawn(Fd, ChildP, Rf),
+      conditional_log(fun cuter_log:log_spawn/3, [Fd, ChildP, Rf], Options),
       mk_result(CC, CC)
   end;
 
 %% spawn_opt/{1,3,4,5}
-eval({named, erlang, spawn_opt}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({named, erlang, spawn_opt}, CAs, SAs, _CallType, Servers, Fd, Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   Rf = erlang:make_ref(),
@@ -259,7 +267,7 @@ eval({named, erlang, spawn_opt}, CAs, SAs, _CallType, Servers, Fd) ->
     end,
   receive
     {ChildP, registered} ->
-      cuter_log:log_spawn(Fd, ChildP, Rf),
+      conditional_log(fun cuter_log:log_spawn/3, [Fd, ChildP, Rf], Options),
       mk_result(R, R)
   end;
 
@@ -267,11 +275,11 @@ eval({named, erlang, spawn_opt}, CAs, SAs, _CallType, Servers, Fd) ->
 %% so as to zip the concrete and symbolic message
 
 %% Redirect erlang:'!'/2 to erlang:send/2
-eval({named, erlang, '!'}, [_, _] = CAs, SAs, CallType, Servers, Fd) ->
-  eval({named, erlang, send}, CAs, SAs, CallType, Servers, Fd);
+eval({named, erlang, '!'}, [_, _] = CAs, SAs, CallType, Servers, Fd, Options) ->
+  eval({named, erlang, send}, CAs, SAs, CallType, Servers, Fd, Options);
 
 %% send/{2,3}
-eval({named, erlang, send}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({named, erlang, send}, CAs, SAs, _CallType, Servers, Fd, _) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
@@ -294,7 +302,7 @@ eval({named, erlang, send}, CAs, SAs, _CallType, Servers, Fd) ->
   end;
 
 %% send_after/3
-eval({named, erlang, send_after}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({named, erlang, send_after}, CAs, SAs, _CallType, Servers, Fd, _Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
@@ -310,7 +318,7 @@ eval({named, erlang, send_after}, CAs, SAs, _CallType, Servers, Fd) ->
   end;
 
 %% send_nosuspend/{2,3}
-eval({named, erlang, send_nosuspend}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({named, erlang, send_nosuspend}, CAs, SAs, _CallType, Servers, Fd, _Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
@@ -336,7 +344,7 @@ eval({named, erlang, send_nosuspend}, CAs, SAs, _CallType, Servers, Fd) ->
 %% so as to zip the concrete and symbolic reason
 
 %% throw/1
-eval({named, erlang, throw}, CAs, SAs, _CallType, _Servers, Fd) ->
+eval({named, erlang, throw}, CAs, SAs, _CallType, _Servers, Fd, _Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
@@ -349,7 +357,7 @@ eval({named, erlang, throw}, CAs, SAs, _CallType, _Servers, Fd) ->
   end;
 
 %% exit/{1,2}
-eval({named, erlang, exit}, CAs, SAs, _CallType, _Servers, Fd) ->
+eval({named, erlang, exit}, CAs, SAs, _CallType, _Servers, Fd, _Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
@@ -380,7 +388,7 @@ eval({named, erlang, exit}, CAs, SAs, _CallType, _Servers, Fd) ->
   end;
 
 %% error/{1,2}
-eval({named, erlang, error}, CAs, SAs, _CallType, _Servers, Fd) ->
+eval({named, erlang, error}, CAs, SAs, _CallType, _Servers, Fd, _Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
@@ -398,7 +406,7 @@ eval({named, erlang, error}, CAs, SAs, _CallType, _Servers, Fd) ->
   end;
 
 %% raise/3
-eval({named, erlang, raise}, CAs, SAs, _CallType, _Servers, Fd) ->
+eval({named, erlang, raise}, CAs, SAs, _CallType, _Servers, Fd, _Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
@@ -414,30 +422,30 @@ eval({named, erlang, raise}, CAs, SAs, _CallType, _Servers, Fd) ->
 %% Handle other important functions
 
 %% make_fun/3
-eval({named, erlang, make_fun}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({named, erlang, make_fun}, CAs, SAs, _CallType, Servers, Fd, Options) ->
   Arity = length(CAs),
   _ = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
     [M, F, A] ->
-      make_fun(M, F, A, Servers, Fd);
+      make_fun(M, F, A, Servers, Fd, Options);
     _ ->
       exception(error, {undef, {erlang, make_fun, Arity}})
   end;
 
 %% apply/{2,3}
-eval({named, erlang, apply}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({named, erlang, apply}, CAs, SAs, _CallType, Servers, Fd, Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   case CAs of
     [Fun, Args] ->
       [SFun, SArgs] = SAs_e,
       %% Constraint: Fun=SFun
-      eval({lambda, Fun, SFun}, Args, SArgs, local, Servers, Fd);
+      eval({lambda, Fun, SFun}, Args, SArgs, local, Servers, Fd, Options);
     [M, F, Args] ->
       [_SMod, _SFun, SArgs] = SAs_e,
       %% Constraints: SMod = M, SFun=F
       Call = find_call_type(erlang, M),
-      eval({named, M, F}, Args, SArgs, Call, Servers, Fd);
+      eval({named, M, F}, Args, SArgs, Call, Servers, Fd, Options);
     _ ->
       exception(error, {undef, {erlang, apply, Arity}})
   end;
@@ -445,7 +453,7 @@ eval({named, erlang, apply}, CAs, SAs, _CallType, Servers, Fd) ->
 %% Generic case
 
 %% Handle an MFA
-eval({named, M, F}, CAs_b, SAs_b, CallType, Servers, Fd) ->
+eval({named, M, F}, CAs_b, SAs_b, CallType, Servers, Fd, Options) ->
   {CAs, SAs} = adjust_arguments(M, F, CAs_b, SAs_b, Fd),
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
@@ -460,11 +468,11 @@ eval({named, M, F}, CAs_b, SAs_b, CallType, Servers, Fd) ->
       NSenv = cuter_env:new_environment(),
       Cenv = cuter_env:bind_parameters(CAs, Code#c_fun.vars, NCenv),
       Senv = cuter_env:bind_parameters(SAs_e, Code#c_fun.vars, NSenv),
-      eval_expr(Code#c_fun.body, NM, Cenv, Senv, Servers, Fd)
+      eval_expr(Code#c_fun.body, NM, Cenv, Senv, Servers, Fd, Options)
   end;
 
 %% Handle a Closure
-eval({lambda, Closure, ClosureSymb}, CAs, SAs, _CallType, _Servers, Fd) ->
+eval({lambda, Closure, ClosureSymb}, CAs, SAs, _CallType, _Servers, Fd, Options) ->
   Arity = length(CAs),
   SAs_e = cuter_symbolic:ensure_list(SAs, Arity, Fd),
   ZAs = zip_args(CAs, SAs_e),
@@ -487,42 +495,49 @@ eval({lambda, Closure, ClosureSymb}, CAs, SAs, _CallType, _Servers, Fd) ->
               mk_result(Cv, R);
             true ->
               Sv = get_symbolic(Cv),
-              cuter_log:log_evaluated_closure(Fd, ClosureSymb, SAs_e, Sv),
+              conditional_log(fun cuter_log:log_evaluated_closure/4, [Fd, ClosureSymb, SAs_e, Sv], Options),
               Cv
           end
       end
   end;
 
 %% Handle a function bound in a letrec expression
-eval({letrec_func, {M, _F, Def, E}}, CAs, SAs, _CallType, Servers, Fd) ->
+eval({letrec_func, {M, _F, Def, E}}, CAs, SAs, _CallType, Servers, Fd, Options) ->
   {Cenv, Senv} = E(),
   SAs_e = cuter_symbolic:ensure_list(SAs, length(CAs), Fd),
   NCenv = cuter_env:bind_parameters(CAs, Def#c_fun.vars, Cenv),
   NSenv = cuter_env:bind_parameters(SAs_e, Def#c_fun.vars, Senv),
-  eval_expr(Def#c_fun.body, M, NCenv, NSenv, Servers, Fd).
+  eval_expr(Def#c_fun.body, M, NCenv, NSenv, Servers, Fd, Options).
 
 %% --------------------------------------------------------
 %% eval_expr
 %%
 %% Evaluates a Core Erlang expression
 %% --------------------------------------------------------
--spec eval_expr(cerl:cerl(), module(), cuter_env:environment(), cuter_env:environment(), servers(), file:io_device()) -> result().
+-spec eval_expr(cerl:cerl(), module(), cuter_env:environment(), cuter_env:environment(), servers(), file:io_device(), eval_opts()) -> result().
 
 %% c_apply
-eval_expr({c_apply, _Anno, Op, Args}, M, Cenv, Senv, Servers, Fd) ->
-  Op_ev = eval_expr(Op, M, Cenv, Senv, Servers, Fd),
+eval_expr({c_apply, Anno, Op, Args}, M, Cenv, Senv, Servers, Fd, Options) ->
+  Op_ev = eval_expr(Op, M, Cenv, Senv, Servers, Fd, Options),
+  DT = cuter_maybe_error_annotation:get_distrust_type_dependent(Anno),
+  case DT of
+    true ->
+      NewOptions = maps:update(distrustTypeDependent, DT, Options);
+    false ->
+      NewOptions = Options
+  end,
   Fun =
     fun(A) ->
-      A_ev = eval_expr(A, M, Cenv, Senv, Servers, Fd),
+      A_ev = eval_expr(A, M, Cenv, Senv, Servers, Fd, NewOptions),
       %% Will create closures where appropriate
       case get_concrete(A_ev) of
         {?FUNCTION_PREFIX, {F, Arity}} ->
           %% local func (external func is already in make_fun/3 in core erlang)
-          create_closure(M, F, Arity, local, Servers, Fd);
+          create_closure(M, F, Arity, local, Servers, Fd, NewOptions);
         {letrec_func, {Mod, F, Arity, Def, E}} ->
           %% letrec func
           {Ce, Se} = E(),
-          create_closure(Mod, F, Arity, {letrec_func, {Def, Ce, Se}}, Servers, Fd);
+          create_closure(Mod, F, Arity, {letrec_func, {Def, Ce, Se}}, Servers, Fd, NewOptions);
         _ ->
           A_ev
       end
@@ -531,37 +546,37 @@ eval_expr({c_apply, _Anno, Op, Args}, M, Cenv, Senv, Servers, Fd) ->
   {CAs, SAs} = cuter_lib:unzip_with(fun to_tuple/1, ZAs),
   case get_concrete(Op_ev) of % See eval_expr(#c_var{}, ...) output for reference
     {?FUNCTION_PREFIX, {Func, _Arity}} ->
-      eval({named, M, Func}, CAs, SAs, local, Servers, Fd);
+      eval({named, M, Func}, CAs, SAs, local, Servers, Fd, NewOptions);
     {letrec_func, {Mod, Func, _Arity, Def, E}} ->
-      eval({letrec_func, {Mod, Func, Def, E}}, CAs, SAs, local, Servers, Fd);
+      eval({letrec_func, {Mod, Func, Def, E}}, CAs, SAs, local, Servers, Fd, NewOptions);
     Closure ->
       %% Constraint OP_s = OP_c (in case closure is made by make_fun)
-      eval({lambda, Closure, get_symbolic(Op_ev)}, CAs, SAs, local, Servers, Fd)
+      eval({lambda, Closure, get_symbolic(Op_ev)}, CAs, SAs, local, Servers, Fd, NewOptions)
   end;
 
 %% c_binary
 %% TODO Use the tags of segments.
-eval_expr({c_binary, _Anno, Segments}, M, Cenv, Senv, Servers, Fd) ->
-  Segs = [eval_expr(S, M, Cenv, Senv, Servers, Fd) || S <- Segments],
+eval_expr({c_binary, _Anno, Segments}, M, Cenv, Senv, Servers, Fd, Options) ->
+  Segs = [eval_expr(S, M, Cenv, Senv, Servers, Fd, Options) || S <- Segments],
   {Cs, Ss} = cuter_lib:unzip_with(fun to_tuple/1, Segs),
   append_segments(Cs, Ss, Fd);
 
 %% c_bitstr
-eval_expr({c_bitstr, _Anno, Val, Size, Unit, Type, Flags}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_bitstr, _Anno, Val, Size, Unit, Type, Flags}, M, Cenv, Senv, Servers, Fd, Options) ->
   %% Evaluate the value and the encoding.
-  Val_ev = eval_expr(Val, M, Cenv, Senv, Servers, Fd),
+  Val_ev = eval_expr(Val, M, Cenv, Senv, Servers, Fd, Options),
   Val_c = get_concrete(Val_ev),
   Val_s = get_symbolic(Val_ev),
-  Size_ev = eval_expr(Size, M, Cenv, Senv, Servers, Fd),
-  Unit_ev = eval_expr(Unit, M, Cenv, Senv, Servers, Fd),
-  Type_ev = eval_expr(Type, M, Cenv, Senv, Servers, Fd),
-  Flags_ev = eval_expr(Flags, M, Cenv, Senv, Servers, Fd),
+  Size_ev = eval_expr(Size, M, Cenv, Senv, Servers, Fd, Options),
+  Unit_ev = eval_expr(Unit, M, Cenv, Senv, Servers, Fd, Options),
+  Type_ev = eval_expr(Type, M, Cenv, Senv, Servers, Fd, Options),
+  Flags_ev = eval_expr(Flags, M, Cenv, Senv, Servers, Fd, Options),
   Size_c = get_concrete(Size_ev),
   Size_s = get_symbolic(Size_ev),
   %% Log constraints on type mismatch before construction.
-  log_bistr_type_mismatch(Val_c, Val_s, Type, Fd), % Type is always a literal.
+  conditional_log(fun log_bistr_type_mismatch/4, [Val_c, Val_s, Type, Fd], Options),  % Type is always a literal.
   %% Log constraints on negative sizes before construction.
-  log_bitstr_neg_size(Size_c, Size_s, Fd),
+  conditional_log(fun log_bitstr_neg_size/3, [Size_c, Size_s, Fd], Options),
   %% Generate the concrete value.
   Bin_c = cuter_binlib:make_bitstring(Val_c, Size_c,
     get_concrete(Unit_ev), get_concrete(Type_ev), get_concrete(Flags_ev)),
@@ -573,21 +588,28 @@ eval_expr({c_bitstr, _Anno, Val, Size, Unit, Type, Flags}, M, Cenv, Senv, Server
   mk_result(Bin_c, Bin_s);
 
 %% c_call
-eval_expr({c_call, _Anno, Mod, Name, Args}, M, Cenv, Senv, Servers, Fd) ->
-  Mod_ev = eval_expr(Mod, M, Cenv, Senv, Servers, Fd),
-  Fv_ev = eval_expr(Name, M, Cenv, Senv, Servers, Fd),
+eval_expr({c_call, Anno, Mod, Name, Args}, M, Cenv, Senv, Servers, Fd, Options) ->
+  Mod_ev = eval_expr(Mod, M, Cenv, Senv, Servers, Fd, Options),
+  Fv_ev = eval_expr(Name, M, Cenv, Senv, Servers, Fd, Options),
+  DT = cuter_maybe_error_annotation:get_distrust_type_dependent(Anno),
+  case DT of
+    true ->
+      NewOptions = maps:update(distrustTypeDependent, true, Options);
+    false ->
+      NewOptions = Options
+  end,
   Fun =
     fun(A) ->
-      A_ev = eval_expr(A, M, Cenv, Senv, Servers, Fd),
+      A_ev = eval_expr(A, M, Cenv, Senv, Servers, Fd, NewOptions),
       %% Will create closures where appropriate
       case get_concrete(A_ev) of
         {?FUNCTION_PREFIX, {F, Arity}} ->
           %% local func (external func is already in make_fun/3 in core erlang)
-          create_closure(M, F, Arity, local, Servers, Fd);
+          create_closure(M, F, Arity, local, Servers, Fd, NewOptions);
         {letrec_func, {Mod, F, Arity, Def, E}} ->
           %% letrec func
           {Ce, Se} = E(),
-          create_closure(Mod, F, Arity, {letrec_func, {Def, Ce, Se}}, Servers, Fd);
+          create_closure(Mod, F, Arity, {letrec_func, {Def, Ce, Se}}, Servers, Fd, NewOptions);
         _ ->
           A_ev
       end
@@ -596,20 +618,27 @@ eval_expr({c_call, _Anno, Mod, Name, Args}, M, Cenv, Senv, Servers, Fd) ->
   {CAs, SAs} = cuter_lib:unzip_with(fun to_tuple/1, ZAs),
   %% Constraints Mod_c = Mod_s and Fv_c = Fv_s
   Mod_c = get_concrete(Mod_ev),
-  eval({named, Mod_c, get_concrete(Fv_ev)}, CAs, SAs, find_call_type(M, Mod_c), Servers, Fd);
+  eval({named, Mod_c, get_concrete(Fv_ev)}, CAs, SAs, find_call_type(M, Mod_c), Servers, Fd, NewOptions);
 
 %% c_case
-eval_expr({c_case, _Anno, Arg, Clauses}, M, Cenv, Senv, Servers, Fd) ->
-  Arg_ev = eval_expr(Arg, M, Cenv, Senv, Servers, Fd),
-  {Body, Ce, Se, _Cnt} = find_clause(Clauses, M, 'case', get_concrete(Arg_ev), get_symbolic(Arg_ev), Cenv, Senv, Servers, Fd),
+eval_expr({c_case, Anno, Arg, Clauses}, M, Cenv, Senv, Servers, Fd, Options) ->
+  DT = maps:get(distrustTypeDependent, Options),
+  NewOptions = maps:update(isForced, cuter_maybe_error_annotation:get_maybe_error_bin_anno(Anno, DT) or maps:get(isForced, Options), Options),
+  Arg_ev = eval_expr(Arg, M, Cenv, Senv, Servers, Fd, NewOptions),
+  {Body, Ce, Se, _Cnt} = find_clause(Clauses, M, 'case', get_concrete(Arg_ev), get_symbolic(Arg_ev), Cenv, Senv, Servers, Fd, NewOptions),
+  NewOptions1 =
+    case not cuter_maybe_error_annotation:get_maybe_error_bin(Body, DT) andalso not maps:get(isForced, Options) of
+      true -> maps:update(constraintLogging, false, Options);
+      false -> Options
+    end,
   cuter_log:reduce_constraint_counter(), % TODO Should also add this call to c_receive
-  eval_expr(Body, M, Ce, Se, Servers, Fd);
+  eval_expr(Body, M, Ce, Se, Servers, Fd, NewOptions1);
 
 %% c_catch
 %% Commented code: allow the exceptions to propagate
-eval_expr({c_catch, _Anno, Body}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_catch, _Anno, Body}, M, Cenv, Senv, Servers, Fd, Options) ->
   try
-    eval_expr(Body, M, Cenv, Senv, Servers, Fd)
+    eval_expr(Body, M, Cenv, Senv, Servers, Fd, Options)
   catch
     throw:Throw ->
       unzip_one(Throw);
@@ -633,22 +662,24 @@ eval_expr({c_catch, _Anno, Body}, M, Cenv, Senv, Servers, Fd) ->
 %%  eval_expr(Body, M, Cenv, Senv, Servers, Fd);
 
 %% c_cons
-eval_expr({c_cons, _Anno, Hd, Tl}, M, Cenv, Senv, Servers, Fd) ->
-  Hd_ev = eval_expr(Hd, M, Cenv, Senv, Servers, Fd),
-  Tl_ev = eval_expr(Tl, M, Cenv, Senv, Servers, Fd),
+eval_expr({c_cons, _Anno, Hd, Tl}, M, Cenv, Senv, Servers, Fd, Options) ->
+  Hd_ev = eval_expr(Hd, M, Cenv, Senv, Servers, Fd, Options),
+  Tl_ev = eval_expr(Tl, M, Cenv, Senv, Servers, Fd, Options),
   Cv = [get_concrete(Hd_ev) | get_concrete(Tl_ev)],
   Sv = cuter_symbolic:cons(get_symbolic(Hd_ev), get_symbolic(Tl_ev), Cv, Fd),
   mk_result(Cv, Sv);
 
 %% c_fun
-eval_expr({c_fun, _Anno, Vars, Body}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_fun, _Anno, Vars, Body}, M, Cenv, Senv, Servers, Fd, Options) ->
   Arity = length(Vars),
-  make_fun(Vars, Body, M, Arity, Cenv, Senv, Servers, Fd);
+  make_fun(Vars, Body, M, Arity, Cenv, Senv, Servers, Fd, Options);
 
 %% c_let
-eval_expr({c_let, _Anno, Vars, Arg, Body}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_let, Anno, Vars, Arg, Body}, M, Cenv, Senv, Servers, Fd, Options) ->
   Deg = length(Vars),
-  Arg_ev = eval_expr(Arg, M, Cenv, Senv, Servers, Fd),
+  IsForced1 = cuter_maybe_error_annotation:get_force_constraint_logging(Anno),
+  NewOptions = maps:update(isForced, IsForced1 orelse maps:get(isForced, Options), Options),
+  Arg_ev = eval_expr(Arg, M, Cenv, Senv, Servers, Fd, NewOptions),
   Arg_c = get_concrete(Arg_ev),
   Arg_s = get_symbolic(Arg_ev),
   case Deg of
@@ -661,10 +692,10 @@ eval_expr({c_let, _Anno, Vars, Arg, Body}, M, Cenv, Senv, Servers, Fd) ->
   end,
   Ce = cuter_env:bind_parameters(CAs, Vars, Cenv),
   Se = cuter_env:bind_parameters(SAs, Vars, Senv),
-  eval_expr(Body, M, Ce, Se, Servers, Fd);
+  eval_expr(Body, M, Ce, Se, Servers, Fd, Options);
 
 %% c_letrec
-eval_expr({c_letrec, _Anno, Defs, Body}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_letrec, _Anno, Defs, Body}, M, Cenv, Senv, Servers, Fd, Options) ->
   H = fun(F) -> fun() ->
     lists:foldl(
       fun({Func, Def}, {E_c, E_s}) ->
@@ -680,10 +711,10 @@ eval_expr({c_letrec, _Anno, Defs, Body}, M, Cenv, Senv, Servers, Fd) ->
     )
   end end,
   {NCe, NSe} = (y(H))(),
-  eval_expr(Body, M, NCe, NSe, Servers, Fd);
+  eval_expr(Body, M, NCe, NSe, Servers, Fd, Options);
 
 %% c_literal
-eval_expr({c_literal, _Anno, V}, _M, _Cenv, _Senv, Servers, Fd) ->
+eval_expr({c_literal, _Anno, V}, _M, _Cenv, _Senv, Servers, Fd, Options) ->
   case erlang:is_function(V) of
     false -> mk_result(V, V);
     true ->
@@ -698,15 +729,15 @@ eval_expr({c_literal, _Anno, V}, _M, _Cenv, _Senv, Servers, Fd) ->
 	      mk_result(V, LambdaS);
 	    Mod ->
 	      Func = proplists:get_value(name, Info),
-	      make_fun(Mod, Func, Arity, Servers, Fd)
+	      make_fun(Mod, Func, Arity, Servers, Fd, Options)
 	  end
       end
   end;
 
 %% c_primop
-eval_expr({c_primop, _Anno, Name, Args}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_primop, _Anno, Name, Args}, M, Cenv, Senv, Servers, Fd, Options) ->
   PrimOp = Name#c_literal.val,
-  ZAs = [eval_expr(A, M, Cenv, Senv, Servers, Fd) || A <- Args],
+  ZAs = [eval_expr(A, M, Cenv, Senv, Servers, Fd, Options) || A <- Args],
   {CAs, SAs} = cuter_lib:unzip_with(fun to_tuple/1, ZAs),
   %% TODO need to record and implement more primops
   %% like 'bs_context_to_binary', 'bs_init_writable'
@@ -715,44 +746,44 @@ eval_expr({c_primop, _Anno, Name, Args}, M, Cenv, Senv, Servers, Fd) ->
       [Class_c, Reason_c] = CAs,
       [_Class_s, Reason_s] = SAs,
       %% CONSTRAINT: Class_c = Class_s
-      eval({named, erlang, Class_c}, [Reason_c], [Reason_s], external, Servers, Fd);
+      eval({named, erlang, Class_c}, [Reason_c], [Reason_s], external, Servers, Fd, Options);
     match_fail ->
       [Cv] = CAs,
       [Sv] = SAs,
-      eval({named, erlang, error}, [{badmatch, Cv}], [{badmatch, Sv}], external, Servers, Fd);
+      eval({named, erlang, error}, [{badmatch, Cv}], [{badmatch, Sv}], external, Servers, Fd, Options);
     _ ->
       exception(error, {primop_not_supported, PrimOp})
   end;
 
 %% c_receive
-eval_expr({c_receive, _Anno, Clauses, Timeout, Action}, M, Cenv, Senv, Servers, Fd) ->
-  Timeout_ev = eval_expr(Timeout, M, Cenv, Senv, Servers, Fd),
+eval_expr({c_receive, _Anno, Clauses, Timeout, Action}, M, Cenv, Senv, Servers, Fd, Options) ->
+  Timeout_ev = eval_expr(Timeout, M, Cenv, Senv, Servers, Fd, Options),
   Timeout_c = get_concrete(Timeout_ev),
   Timeout_s = get_symbolic(Timeout_ev),
   true = check_timeout(Timeout_c, Timeout_s, Fd),
   Start = os:timestamp(),  %% Start time of timeout timer
   {messages, Mailbox} = erlang:process_info(self(), messages),
-  Message = find_message(Mailbox, Clauses, M, Cenv, Senv, Servers, Fd),
+  Message = find_message(Mailbox, Clauses, M, Cenv, Senv, Servers, Fd, Options),
   case Message of
     {Msg, Body, NCenv, NSenv, _Cnt} ->  %% Matched a message already in the mailbox
       receive Msg -> ok end,  %% Just consume the message
-      eval_expr(Body, M, NCenv, NSenv, Servers, Fd);
+      eval_expr(Body, M, NCenv, NSenv, Servers, Fd, Options);
     false ->  %% No mailbox message matched, thus need to enter a receive loop
       CurrMsgs = length(Mailbox),
-      find_message_loop(Clauses, Action, Timeout_c, Timeout_s, Start, CurrMsgs, M, Cenv, Senv, Servers, Fd)
+      find_message_loop(Clauses, Action, Timeout_c, Timeout_s, Start, CurrMsgs, M, Cenv, Senv, Servers, Fd, Options)
   end;
 
 %% c_seq
-eval_expr({c_seq, _Anno, Arg, Body}, M, Cenv, Senv, Servers, Fd) ->
-  _ = eval_expr(Arg, M, Cenv, Senv, Servers, Fd),
-  eval_expr(Body, M, Cenv, Senv, Servers, Fd);
+eval_expr({c_seq, _Anno, Arg, Body}, M, Cenv, Senv, Servers, Fd, Options) ->
+  _ = eval_expr(Arg, M, Cenv, Senv, Servers, Fd, Options),
+  eval_expr(Body, M, Cenv, Senv, Servers, Fd, Options);
 
 %% c_try
 %% Commented code: allow the exceptions to propagate
-eval_expr({c_try, _Anno, Arg, Vars, Body, Evars, Handler}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_try, _Anno, Arg, Vars, Body, Evars, Handler}, M, Cenv, Senv, Servers, Fd, Options) ->
   try
     Deg = length(Vars),
-    A_ev = eval_expr(Arg, M, Cenv, Senv, Servers, Fd),
+    A_ev = eval_expr(Arg, M, Cenv, Senv, Servers, Fd, Options),
     A_c = get_concrete(A_ev),
     A_s = get_concrete(A_ev),
     case Deg of
@@ -765,7 +796,7 @@ eval_expr({c_try, _Anno, Arg, Vars, Body, Evars, Handler}, M, Cenv, Senv, Server
     end,
     Ce = cuter_env:bind_parameters(CAs, Vars, Cenv),
     Se = cuter_env:bind_parameters(SAs, Vars, Senv),
-    eval_expr(Body, M, Ce, Se, Servers, Fd)
+    eval_expr(Body, M, Ce, Se, Servers, Fd, Options)
   catch
     Class:Reason ->
       Reason1 = unzip_one(Reason),
@@ -783,7 +814,7 @@ eval_expr({c_try, _Anno, Arg, Vars, Body, Evars, Handler}, M, Cenv, Senv, Server
         end,
       ECe = cuter_env:bind_parameters(Cs, Evars, Cenv),
       ESe = cuter_env:bind_parameters(Ss, Evars, Senv),
-      eval_expr(Handler, M, ECe, ESe, Servers, Fd)
+      eval_expr(Handler, M, ECe, ESe, Servers, Fd, Options)
   end;
 %%eval_expr({c_try, _Anno, Arg, Vars, Body, _Evars, _Handler}, M, Cenv, Senv, Servers, Fd) ->
 %%  Deg = length(Vars),
@@ -801,24 +832,24 @@ eval_expr({c_try, _Anno, Arg, Vars, Body, Evars, Handler}, M, Cenv, Senv, Server
 %%  eval_expr(Body, M, Ce, Se, Servers, Fd);
 
 %% c_tuple
-eval_expr({c_tuple, _Anno, Es}, M, Cenv, Senv, Servers, Fd) ->
-  Zes = [eval_expr(E, M, Cenv, Senv, Servers, Fd) || E <- Es],
+eval_expr({c_tuple, _Anno, Es}, M, Cenv, Senv, Servers, Fd, Options) ->
+  Zes = [eval_expr(E, M, Cenv, Senv, Servers, Fd, Options) || E <- Es],
   {Es_c, Es_s} = cuter_lib:unzip_with(fun to_tuple/1, Zes),
   Cv = list_to_tuple(Es_c),
   Sv = cuter_symbolic:make_tuple(Es_s, Cv, Fd),
   mk_result(Cv, Sv);
 
 %% c_values
-eval_expr({c_values, _Anno, Es}, M, Cenv, Senv, Servers, Fd) ->
+eval_expr({c_values, _Anno, Es}, M, Cenv, Senv, Servers, Fd, Options) ->
   Deg = length(Es),
-  Zes = [eval_expr(E, M, Cenv, Senv, Servers, Fd) || E <- Es],
+  Zes = [eval_expr(E, M, Cenv, Senv, Servers, Fd, Options) || E <- Es],
   {Es_c, Es_s} = cuter_lib:unzip_with(fun to_tuple/1, Zes),
   Cv = #valuelist{values=Es_c, degree=Deg},
   Sv = #valuelist{values=Es_s, degree=Deg},
   mk_result(Cv, Sv);
 
 %% c_var
-eval_expr({c_var, _Anno, Name}, _M, Cenv, Senv, _Servers, _Fd) when is_tuple(Name) ->
+eval_expr({c_var, _Anno, Name}, _M, Cenv, Senv, _Servers, _Fd, _Options) when is_tuple(Name) ->
   %% If Name is a function
   case cuter_env:get_value(Name, Cenv) of
     {ok, {letrec_func, {Mod, Def, E}}} ->
@@ -835,13 +866,13 @@ eval_expr({c_var, _Anno, Name}, _M, Cenv, Senv, _Servers, _Fd) when is_tuple(Nam
       R = {?FUNCTION_PREFIX, Name},
       mk_result(R, R)
   end;
-eval_expr({c_var, _Anno, Name}, _M, Cenv, Senv, _Servers, _Fd) ->
+eval_expr({c_var, _Anno, Name}, _M, Cenv, Senv, _Servers, _Fd, _Options) ->
   %% If it's a variable then return its value
   {ok, Cv} = cuter_env:get_value(Name, Cenv),
   {ok, Sv} = cuter_env:get_value(Name, Senv),
   mk_result(Cv, Sv);
 
-eval_expr(Cerl, _M, _Cenv, _Senv, _Servers, _Fd) ->
+eval_expr(Cerl, _M, _Cenv, _Senv, _Servers, _Fd, _Options) ->
   exception(error, {unknown_cerl, Cerl}).
 
 
@@ -950,16 +981,16 @@ exception(Class, Reason) ->
 %% Enters a loop waiting for a message that will match.
 %% Wraps calls to run_message_loop to check for timeout.
 %% --------------------------------------------------------
-find_message_loop(Clauses, Action, infinity, STimetout, Start, Msgs, M, Cenv, Senv, Servers, Fd) ->
-  run_message_loop(Clauses, Action, infinity, STimetout, Start, Msgs, M, Cenv, Senv, Servers, Fd);
-find_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd) ->
+find_message_loop(Clauses, Action, infinity, STimetout, Start, Msgs, M, Cenv, Senv, Servers, Fd, Options) ->
+  run_message_loop(Clauses, Action, infinity, STimetout, Start, Msgs, M, Cenv, Senv, Servers, Fd, Options);
+find_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd, Options) ->
   Now = os:timestamp(),
   Passed = timer:now_diff(Now, Start) / 1000,
   case Passed >= CTimeout of
     true ->
-      eval_expr(Action, M, Cenv, Senv, Servers, Fd);
+      eval_expr(Action, M, Cenv, Senv, Servers, Fd, Options);
     false ->
-      run_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd)
+      run_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd, Options)
   end.
 
 %% --------------------------------------------------------
@@ -967,23 +998,23 @@ find_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Sen
 %%
 %% Implements the actual waiting receive loop
 %% --------------------------------------------------------
-run_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd) ->
+run_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd, Options) ->
   erlang:yield(),
   {message_queue_len, CurrMsgs} = erlang:process_info(self(), message_queue_len),
   %% New messages will appended at the end of the mailbox
   case CurrMsgs > Msgs of
     false -> %% No new messages
-      find_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd);
+      find_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv, Servers, Fd, Options);
     true ->
       {messages, Mailbox} = erlang:process_info(self(), messages),
       NewMsgs = lists:nthtail(Msgs, Mailbox),
-      Message = find_message(NewMsgs, Clauses, M, Cenv, Senv, Servers, Fd),
+      Message = find_message(NewMsgs, Clauses, M, Cenv, Senv, Servers, Fd, Options),
       case Message of
         false ->
-          find_message_loop(Clauses, Action, CTimeout, STimeout, Start, CurrMsgs, M, Cenv, Senv, Servers, Fd);
+          find_message_loop(Clauses, Action, CTimeout, STimeout, Start, CurrMsgs, M, Cenv, Senv, Servers, Fd, Options);
         {Msg, Body, NCenv, NSenv, _Cnt} ->
           receive Msg -> ok end,  %% Just consume the matched message
-          eval_expr(Body, M, NCenv, NSenv, Servers, Fd)
+          eval_expr(Body, M, NCenv, NSenv, Servers, Fd, Options)
       end
   end.
 
@@ -993,16 +1024,16 @@ run_message_loop(Clauses, Action, CTimeout, STimeout, Start, Msgs, M, Cenv, Senv
 %% Wraps calls to find_clause when trying to match 
 %% a message against a series of patterns
 %% --------------------------------------------------------
-find_message([], _Clauses, _M, _Cenv, _Senv, _Servers, _Fd) ->
+find_message([], _Clauses, _M, _Cenv, _Senv, _Servers, _Fd, _Options) ->
   false;
 
-find_message([Msg|Mailbox], Clauses, M, Cenv, Senv, Servers, Fd) ->
+find_message([Msg|Mailbox], Clauses, M, Cenv, Senv, Servers, Fd, Options) ->
   {LoggerFun, Msg1} = decode_msg(Msg, Fd),
-  case find_clause(Clauses, M, 'receive', get_concrete(Msg1), get_symbolic(Msg1), Cenv, Senv, Servers, Fd) of
+  case find_clause(Clauses, M, 'receive', get_concrete(Msg1), get_symbolic(Msg1), Cenv, Senv, Servers, Fd, Options) of
     false ->
-      find_message(Mailbox, Clauses, M, Cenv, Senv, Servers, Fd);
+      find_message(Mailbox, Clauses, M, Cenv, Senv, Servers, Fd, Options);
     {Body, NCenv, NSenv, Cnt} ->
-      log_successful_msg_match(LoggerFun),
+      conditional_log(fun log_successful_msg_match/1, [LoggerFun], Options),
       %% I can log the received Msg here
       {Msg, Body, NCenv, NSenv, Cnt}
   end.
@@ -1021,16 +1052,16 @@ log_successful_msg_match({withLogger, Fun}) -> Fun().
 %% compiler adds a catch all clause at the end of every
 %% case statement.
 %% --------------------------------------------------------
-find_clause(Clauses, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd) ->
-  find_clause(Clauses, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, 1).
+find_clause(Clauses, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Options) ->
+  find_clause(Clauses, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, 1, Options).
 
-find_clause([], _M, _Mode, _Cv, _Sv, _Cenv, _Senv, _Servers, _Fd, _Cnt) ->
+find_clause([], _M, _Mode, _Cv, _Sv, _Cenv, _Senv, _Servers, _Fd, _Cnt, _Options) ->
   false;
-find_clause([Cl|Cls], M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Cnt) ->
-  Match = match_clause(Cl, M, Mode, Cv, Sv, Cenv, Senv, Servers,  Fd, Cnt),
+find_clause([Cl|Cls], M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Cnt, Options) ->
+  Match = match_clause(Cl, M, Mode, Cv, Sv, Cenv, Senv, Servers,  Fd, Cnt, Options),
   case Match of
     false ->
-      find_clause(Cls, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Cnt+1);
+      find_clause(Cls, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Cnt+1, Options);
     {true, {_Body, _NCenv, _NSenv, Cnt} = Matched} ->
       Matched
   end.
@@ -1041,7 +1072,7 @@ find_clause([Cl|Cls], M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Cnt) ->
 %% Match a pair of concrete & symbolic values against
 %% a specific clause (i.e. with patterns and guard)
 %% --------------------------------------------------------
-match_clause({c_clause, Anno, Pats, Guard, Body}, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Cnt) ->
+match_clause({c_clause, Anno, Pats, Guard, Body}, M, Mode, Cv, Sv, Cenv, Senv, Servers, Fd, Cnt, Options) ->
   case is_patlist_compatible(Pats, Cv) of
     false -> false;
     true ->
@@ -1057,7 +1088,7 @@ match_clause({c_clause, Anno, Pats, Guard, Body}, M, Mode, Cv, Sv, Cenv, Senv, S
       %% BitInfo is needed for parameterized bit-syntax patterns
       BitInfo = {M, Cenv, Senv},
       Ss_e = cuter_symbolic:ensure_list(Ss, length(Cs), Fd),
-      Match = pattern_match_all(Pats, BitInfo, Mode, Cs, Ss_e, Servers, Fd),
+      Match = pattern_match_all(Pats, BitInfo, Mode, Cs, Ss_e, Servers, Fd, Options),
       case Match of
         false -> false;
         {true, {CMs, SMs}} ->
@@ -1065,17 +1096,17 @@ match_clause({c_clause, Anno, Pats, Guard, Body}, M, Mode, Cv, Sv, Cenv, Senv, S
           Se = cuter_env:add_mappings_to_environment(SMs, Senv),
           %% Make silent guards
           Tags = cuter_cerl:get_tags(Anno),
-          Guard_ev = eval_expr(Guard, M, Ce, Se, Servers, Fd),
+          Guard_ev = eval_expr(Guard, M, Ce, Se, Servers, Fd, Options),
           try to_tuple(Guard_ev) of
             {true, SGv} ->
               %% CONSTRAINT: SGv is a True guard
               visit_tag(Servers#svs.code, Tags#tags.this),
-              cuter_log:log_guard(Fd, true, SGv, Tags#tags.next),
+              conditional_log(fun cuter_log:log_guard/4, [Fd, true, SGv, Tags#tags.next], Options),
               {true, {Body, Ce, Se, Cnt}};
             {false, SGv} ->
               %% CONSTRAINT: SGv is a False guard
               visit_tag(Servers#svs.code, Tags#tags.next),
-              cuter_log:log_guard(Fd, false, SGv, Tags#tags.this),
+              conditional_log(fun cuter_log:log_guard/4, [Fd, false, SGv, Tags#tags.this], Options),
               false
           catch
             error:_E -> false
@@ -1090,17 +1121,17 @@ match_clause({c_clause, Anno, Pats, Guard, Body}, M, Mode, Cv, Sv, Cenv, Senv, S
 %% patterns (short-circuited match)
 %% --------------------------------------------------------
 
-pattern_match_all(Pats, BitInfo, Mode, Cs, Ss, Servers, Fd) ->
-  pattern_match_all(Pats, BitInfo, Mode, Cs, Ss, [], [], Servers, Fd).
+pattern_match_all(Pats, BitInfo, Mode, Cs, Ss, Servers, Fd, Options) ->
+  pattern_match_all(Pats, BitInfo, Mode, Cs, Ss, [], [], Servers, Fd, Options).
 
-pattern_match_all([], _BitInfo, _Mode, [], [], CMaps, SMaps, _Servers, _Fd) ->
+pattern_match_all([], _BitInfo, _Mode, [], [], CMaps, SMaps, _Servers, _Fd, _Options) ->
   {true, {CMaps, SMaps}};
-pattern_match_all([P|Ps], BitInfo, Mode, [Cv|Cvs], [Sv|Svs], CMaps, SMaps, Servers, Fd) ->
-  Match = pattern_match(P, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd),
+pattern_match_all([P|Ps], BitInfo, Mode, [Cv|Cvs], [Sv|Svs], CMaps, SMaps, Servers, Fd, Options) ->
+  Match = pattern_match(P, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd, Options),
   case Match of
     false -> false;
     {true, {CMs, SMs}} ->
-      pattern_match_all(Ps, BitInfo, Mode, Cvs, Svs, CMs, SMs, Servers, Fd)
+      pattern_match_all(Ps, BitInfo, Mode, Cvs, Svs, CMs, SMs, Servers, Fd, Options)
   end.
 
 %% --------------------------------------------------------
@@ -1111,29 +1142,29 @@ pattern_match_all([P|Ps], BitInfo, Mode, [Cv|Cvs], [Sv|Svs], CMaps, SMaps, Serve
 %% --------------------------------------------------------
 
 %% AtomicLiteral pattern
-pattern_match({c_literal, Anno, LitVal}, _Bitinfo, _Mode, Cv, Sv, CMaps, SMaps, Servers, Fd) ->
+pattern_match({c_literal, Anno, LitVal}, _Bitinfo, _Mode, Cv, Sv, CMaps, SMaps, Servers, Fd, Options) ->
   Tags = cuter_cerl:get_tags(Anno),
   case LitVal =:= Cv of
     true ->
       %% CONSTRAINT: Sv =:= Litval
       visit_tag(Servers#svs.code, Tags#tags.this),
-      log_literal_match_success(Fd, LitVal, Sv, Tags#tags.next),
+      conditional_log(fun log_literal_match_success/4, [Fd, LitVal, Sv, Tags#tags.next], Options),
       {true, {CMaps, SMaps}};
     false ->
       %% CONSTRAINT: Sv =/= Litval
       visit_tag(Servers#svs.code, Tags#tags.next),
-      log_literal_match_failure(Fd, LitVal, Sv, Tags#tags.this),
+      conditional_log(fun log_literal_match_failure/4, [Fd, LitVal, Sv, Tags#tags.this], Options),
       false
   end;
 
 %% VariableName pattern
-pattern_match({c_var, _Anno, Name}, _BitInfo, _Mode, Cv, Sv, CMaps, SMaps, _Servers, _Fd) ->
+pattern_match({c_var, _Anno, Name}, _BitInfo, _Mode, Cv, Sv, CMaps, SMaps, _Servers, _Fd, _Options) ->
   CMs = [{Name, Cv}|CMaps],
   SMs = [{Name, Sv}|SMaps],
   {true, {CMs, SMs}};
 
 %% Tuple pattern
-pattern_match({c_tuple, Anno, Es}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd) when is_tuple(Cv) ->
+pattern_match({c_tuple, Anno, Es}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd, Options) when is_tuple(Cv) ->
   Ne = length(Es),
   Tags = cuter_cerl:get_tags(Anno),
   case tuple_size(Cv) =:= Ne of
@@ -1141,51 +1172,51 @@ pattern_match({c_tuple, Anno, Es}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers,
       Cv_l = tuple_to_list(Cv),
       %% CONSTRAINT: Sv is a tuple of Ne elements
       visit_tag(Servers#svs.code, Tags#tags.this),
-      cuter_log:log_tuple(Fd, sz, Sv, Ne, Tags#tags.next),
+      conditional_log(fun cuter_log:log_tuple/5, [Fd, sz, Sv, Ne, Tags#tags.next], Options),
       Sv_l = cuter_symbolic:tpl_to_list(Sv, Ne, Fd),
-      pattern_match_all(Es, BitInfo, Mode, Cv_l, Sv_l, CMaps, SMaps, Servers, Fd);
+      pattern_match_all(Es, BitInfo, Mode, Cv_l, Sv_l, CMaps, SMaps, Servers, Fd, Options);
     false ->
       %% CONSTRAINT: Sv is a tuple of not Ne elements
       visit_tag(Servers#svs.code, Tags#tags.next),
-      cuter_log:log_tuple(Fd, not_sz, Sv, Ne, Tags#tags.this),
+      conditional_log(fun cuter_log:log_tuple/5, [Fd, not_sz, Sv, Ne, Tags#tags.this], Options),
       false
   end;
-pattern_match({c_tuple, Anno, Es}, _BitInfo, _Mode, _Cv, Sv, _CMaps, _SMaps, Servers, Fd) ->
+pattern_match({c_tuple, Anno, Es}, _BitInfo, _Mode, _Cv, Sv, _CMaps, _SMaps, Servers, Fd, Options) ->
   Ne = length(Es),
   Tags = cuter_cerl:get_tags(Anno),
   %% CONSTRAINT: Sv is not a tuple
   visit_tag(Servers#svs.code, Tags#tags.next),
-  cuter_log:log_tuple(Fd, not_tpl, Sv, Ne, Tags#tags.this),
+  conditional_log(fun cuter_log:log_tuple/5, [Fd, not_tpl, Sv, Ne, Tags#tags.this], Options),
   false;
 
 %% List constructor pattern
-pattern_match({c_cons, Anno, _Hd, _Tl}, _BitInfo, _Mode, [], Sv, _CMaps, _SMaps, Servers, Fd) ->
+pattern_match({c_cons, Anno, _Hd, _Tl}, _BitInfo, _Mode, [], Sv, _CMaps, _SMaps, Servers, Fd, Options) ->
   Tags = cuter_cerl:get_tags(Anno),
   %% CONSTRAINT: Sv is an empty list
   visit_tag(Servers#svs.code, Tags#tags.next),
-  cuter_log:log_list(Fd, empty, Sv, Tags#tags.this),
+  conditional_log(fun cuter_log:log_list/4, [Fd, empty, Sv, Tags#tags.this], Options),
   false;
-pattern_match({c_cons, Anno, Hd, Tl}, BitInfo, Mode, [Cv|Cvs], Sv, CMaps, SMaps, Servers, Fd) ->
+pattern_match({c_cons, Anno, Hd, Tl}, BitInfo, Mode, [Cv|Cvs], Sv, CMaps, SMaps, Servers, Fd, Options) ->
   Tags = cuter_cerl:get_tags(Anno),
   %% CONSTRAINT: S is a non empty list
   visit_tag(Servers#svs.code, Tags#tags.this),
-  cuter_log:log_list(Fd, nonempty, Sv, Tags#tags.next),
+  conditional_log(fun cuter_log:log_list/4, [Fd, nonempty, Sv, Tags#tags.next], Options),
   Sv_h = cuter_symbolic:head(Sv, Fd),
   Sv_t = cuter_symbolic:tail(Sv, Fd),
-  case pattern_match(Hd, BitInfo, Mode, Cv, Sv_h, CMaps, SMaps, Servers, Fd) of
+  case pattern_match(Hd, BitInfo, Mode, Cv, Sv_h, CMaps, SMaps, Servers, Fd, Options) of
     false -> false;
-    {true, {CMs, SMs}} -> pattern_match(Tl, BitInfo, Mode, Cvs, Sv_t, CMs, SMs, Servers, Fd)
+    {true, {CMs, SMs}} -> pattern_match(Tl, BitInfo, Mode, Cvs, Sv_t, CMs, SMs, Servers, Fd, Options)
   end;
-pattern_match({c_cons, Anno, _Hd, _Tl}, _BitInfo, _Mode, _Cv, Sv, _CMaps, _SMaps, Servers, Fd) ->
+pattern_match({c_cons, Anno, _Hd, _Tl}, _BitInfo, _Mode, _Cv, Sv, _CMaps, _SMaps, Servers, Fd, Options) ->
   Tags = cuter_cerl:get_tags(Anno),
   %% CONSTRAINT: Sv is not a list
   visit_tag(Servers#svs.code, Tags#tags.next),
-  cuter_log:log_list(Fd, not_lst, Sv, Tags#tags.this),
+  conditional_log(fun cuter_log:log_list/4, [Fd, not_lst, Sv, Tags#tags.this], Options),
   false;
 
 %% Alias pattern
-pattern_match({c_alias, _Anno, Var, Pat}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd) ->
-  Match = pattern_match(Pat, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd),
+pattern_match({c_alias, _Anno, Var, Pat}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd, Options) ->
+  Match = pattern_match(Pat, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd, Options),
   case Match of
     false -> false;
     {true, {CMs, SMs}} ->
@@ -1196,43 +1227,43 @@ pattern_match({c_alias, _Anno, Var, Pat}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, S
   end;
 
 %% Binary pattern
-pattern_match({c_binary, Anno, Segments}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd) ->
-  bit_pattern_match(Anno, Segments, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd).
+pattern_match({c_binary, Anno, Segments}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd, Options) ->
+  bit_pattern_match(Anno, Segments, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd, Options).
 
 %% --------------------------------------------------------
 %% bit_pattern_match
 %% 
 %% --------------------------------------------------------
 
-bit_pattern_match(BinAnno, [], _BitInfo, _Mode, <<>>, Sv, CMaps, SMaps, Servers, Fd) ->
+bit_pattern_match(BinAnno, [], _BitInfo, _Mode, <<>>, Sv, CMaps, SMaps, Servers, Fd, Options) ->
   %% CONSTRAINT: Sv =:= <<>>
   Tags = cuter_cerl:get_tags(BinAnno),
   visit_tag(Servers#svs.code, Tags#tags.this),
-  cuter_log:log_equal(Fd, true, <<>>, Sv, Tags#tags.next),
+  conditional_log(fun cuter_log:log_equal/5, [Fd, true, <<>>, Sv, Tags#tags.next], Options),
   {true, {CMaps, SMaps}};
-bit_pattern_match(BinAnno, [], _BitInfo, _Mode, _Cv, Sv, _CMaps, _SMaps, Servers, Fd) ->
+bit_pattern_match(BinAnno, [], _BitInfo, _Mode, _Cv, Sv, _CMaps, _SMaps, Servers, Fd, Options) ->
   %% CONSTRAINT: Sv =/= <<>>
   Tags = cuter_cerl:get_tags(BinAnno),
   visit_tag(Servers#svs.code, Tags#tags.next),
-  cuter_log:log_equal(Fd, false, <<>>, Sv, Tags#tags.this),
+  conditional_log(fun cuter_log:log_equal/5, [Fd, false, <<>>, Sv, Tags#tags.this], Options),
   false;
 
-bit_pattern_match(BinAnno, [{c_bitstr, Anno, {c_literal, _, LVal}, Sz, Unit, Tp, Fgs}|Bs], {M, Cenv, Senv} = Bnfo, Mode, Cv, Sv, CMaps, SMaps, Svs, Fd) ->
-  Size_ev = eval_expr(Sz, M, Cenv, Senv, Svs, Fd),
-  Unit_ev = eval_expr(Unit, M, Cenv, Senv, Svs, Fd),
-  Type_ev = eval_expr(Tp, M, Cenv, Senv, Svs, Fd),
-  Flags_ev = eval_expr(Fgs, M, Cenv, Senv, Svs, Fd),
+bit_pattern_match(BinAnno, [{c_bitstr, Anno, {c_literal, _, LVal}, Sz, Unit, Tp, Fgs}|Bs], {M, Cenv, Senv} = Bnfo, Mode, Cv, Sv, CMaps, SMaps, Svs, Fd, Options) ->
+  Size_ev = eval_expr(Sz, M, Cenv, Senv, Svs, Fd, Options),
+  Unit_ev = eval_expr(Unit, M, Cenv, Senv, Svs, Fd, Options),
+  Type_ev = eval_expr(Tp, M, Cenv, Senv, Svs, Fd, Options),
+  Flags_ev = eval_expr(Fgs, M, Cenv, Senv, Svs, Fd, Options),
   Size_c = get_concrete(Size_ev),
   Size_s = get_symbolic(Size_ev),
   Enc_s = {Size_s, get_symbolic(Unit_ev), get_symbolic(Type_ev), get_symbolic(Flags_ev)},
   Tags = cuter_cerl:get_tags(Anno),
   %% Log constraints on negative sizes before matching.
-  log_bitstr_neg_size(Size_c, Size_s, Fd),
+  conditional_log(fun log_bitstr_neg_size/3, [Size_c, Size_s, Fd], Options),
   try cuter_binlib:match_bitstring_const(LVal, Size_c, get_concrete(Unit_ev), get_concrete(Type_ev), get_concrete(Flags_ev), Cv) of
     Rest_c ->
       visit_tag(Svs#svs.code, Tags#tags.this),
       Rest_s = cuter_symbolic:match_bitstring_const_true(LVal, Enc_s, Sv, Rest_c, Size_c, Tags#tags.next, Fd),
-      bit_pattern_match(BinAnno, Bs, Bnfo, Mode,  Rest_c, Rest_s, CMaps, SMaps, Svs, Fd)
+      bit_pattern_match(BinAnno, Bs, Bnfo, Mode,  Rest_c, Rest_s, CMaps, SMaps, Svs, Fd, Options)
   catch
     error:_e ->
       visit_tag(Svs#svs.code, Tags#tags.next),
@@ -1240,17 +1271,17 @@ bit_pattern_match(BinAnno, [{c_bitstr, Anno, {c_literal, _, LVal}, Sz, Unit, Tp,
       false
   end;
 
-bit_pattern_match(BinAnno, [{c_bitstr, Anno, {c_var, _, VarName}, Sz, Unit, Tp, Fgs}|Bs], {M, Cenv, Senv}, Mode, Cv, Sv, CMaps, SMaps, Svs, Fd) ->
-  Size_ev = eval_expr(Sz, M, Cenv, Senv, Svs, Fd),
-  Unit_ev = eval_expr(Unit, M, Cenv, Senv, Svs, Fd),
-  Type_ev = eval_expr(Tp, M, Cenv, Senv, Svs, Fd),
-  Flags_ev = eval_expr(Fgs, M, Cenv, Senv, Svs, Fd),
+bit_pattern_match(BinAnno, [{c_bitstr, Anno, {c_var, _, VarName}, Sz, Unit, Tp, Fgs}|Bs], {M, Cenv, Senv}, Mode, Cv, Sv, CMaps, SMaps, Svs, Fd, Options) ->
+  Size_ev = eval_expr(Sz, M, Cenv, Senv, Svs, Fd, Options),
+  Unit_ev = eval_expr(Unit, M, Cenv, Senv, Svs, Fd, Options),
+  Type_ev = eval_expr(Tp, M, Cenv, Senv, Svs, Fd, Options),
+  Flags_ev = eval_expr(Fgs, M, Cenv, Senv, Svs, Fd, Options),
   Size_c = get_concrete(Size_ev),
   Size_s = get_symbolic(Size_ev),
   Enc_s = {Size_s, get_symbolic(Unit_ev), get_symbolic(Type_ev), get_symbolic(Flags_ev)},
   Tags = cuter_cerl:get_tags(Anno),
   %% Log constraints on negative sizes before matching.
-  log_bitstr_neg_size(Size_c, Size_s, Fd),
+  conditional_log(fun log_bitstr_neg_size/3, [Size_c, Size_s, Fd], Options),
   try cuter_binlib:match_bitstring_var(Size_c, get_concrete(Unit_ev), get_concrete(Type_ev), get_concrete(Flags_ev), Cv) of
     {X_c, Rest_c} ->
       visit_tag(Svs#svs.code, Tags#tags.this),
@@ -1266,7 +1297,7 @@ bit_pattern_match(BinAnno, [{c_bitstr, Anno, {c_var, _, VarName}, Sz, Unit, Tp,
         end,
       NCenv = cuter_env:add_binding(VarName, X_c, Cenv),
       NSenv = cuter_env:add_binding(VarName, X_s, Senv),
-      bit_pattern_match(BinAnno, Bs, {M, NCenv, NSenv}, Mode, Rest_c, Rest_s, CMs, SMs, Svs, Fd)
+      bit_pattern_match(BinAnno, Bs, {M, NCenv, NSenv}, Mode, Rest_c, Rest_s, CMs, SMs, Svs, Fd, Options)
   catch
     error:_E ->
       visit_tag(Svs#svs.code, Tags#tags.next),
@@ -1280,18 +1311,18 @@ bit_pattern_match(BinAnno, [{c_bitstr, Anno, {c_var, _, VarName}, Sz, Unit, Tp,
 %% --------------------------------------------------------
 
 %% Create a Closure of a local function
-create_closure(M, F, Arity, local, Servers, Fd) ->
+create_closure(M, F, Arity, local, Servers, Fd, Options) ->
   Mfa = {NM, _NF, NA} = cuter_mock:maybe_override_mfa({M, F, Arity}),
   %% Module is already loaded since create_closure is called by eval_expr.
   {ok, Kfun} = get_kfun(Mfa, Servers),
   Code = cuter_cerl:kfun_code(Kfun),
   Cenv = cuter_env:new_environment(),
   Senv = cuter_env:new_environment(),
-  make_fun(Code#c_fun.vars, Code#c_fun.body, NM, NA, Cenv, Senv, Servers, Fd);
+  make_fun(Code#c_fun.vars, Code#c_fun.body, NM, NA, Cenv, Senv, Servers, Fd, Options);
 
 %% Create a Closure when the MFA is a function bound in a letrec
-create_closure(M, _F, Arity, {letrec_func, {Def, Cenv, Senv}}, Servers, Fd) ->
-  make_fun(Def#c_fun.vars, Def#c_fun.body, M, Arity, Cenv, Senv, Servers, Fd).
+create_closure(M, _F, Arity, {letrec_func, {Def, Cenv, Senv}}, Servers, Fd, Options) ->
+  make_fun(Def#c_fun.vars, Def#c_fun.body, M, Arity, Cenv, Senv, Servers, Fd, Options).
 
 %% --------------------------------------------------------
 %% Create closures.
@@ -1304,7 +1335,7 @@ create_closure(M, _F, Arity, {letrec_func, {Def, Cenv, Senv}}, Servers, Fd) ->
 
 %% Creates a closure from Core Erlang code. 
 %% The interpreted code is wrapped in a call to eval_expr.
-make_fun(Vars, Body, Mod, Arity, Cenv, Senv, Servers, Fd) ->
+make_fun(Vars, Body, Mod, Arity, Cenv, Senv, Servers, Fd, Options) ->
   Creator = self(),
   LambdaS = cuter_symbolic:fresh_lambda(Arity, Fd),
   add_to_created_closure(LambdaS),
@@ -1312,94 +1343,94 @@ make_fun(Vars, Body, Mod, Arity, Cenv, Senv, Servers, Fd) ->
     case Arity of
       0 ->
         fun() ->
-          make_fun_h1(Mod, [], Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, [], Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       1 ->
         fun(A) ->
           Args = [A],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       2 ->
         fun(A, B) ->
           Args = [A, B],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       3 ->
         fun(A, B, C) ->
           Args = [A, B, C],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       4 ->
         fun(A, B, C, D) ->
           Args = [A, B, C, D],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       5 ->
         fun(A, B, C, D, E) ->
           Args = [A, B, C, D, E],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       6 ->
         fun(A, B, C, D, E, F) ->
           Args = [A, B, C, D, E, F],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       7 ->
         fun(A, B, C, D, E, F, G) ->
           Args = [A, B, C, D, E, F, G],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       8 ->
         fun(A, B, C, D, E, F, G, H) ->
           Args = [A, B, C, D, E, F, G, H],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       9 ->
         fun(A, B, C, D, E, F, G, H, I) ->
           Args = [A, B, C, D, E, F, G, H, I],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       10 ->
         fun(A, B, C, D, E, F, G, H, I, J) ->
           Args = [A, B, C, D, E, F, G, H, I, J],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       11 ->
         fun(A, B, C, D, E, F, G, H, I, J, K) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       12 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       13 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L, M) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L, M],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       14 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L, M, N) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L, M, N],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       15 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L, M, N, O],
-          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd)
+          make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, Fd, Options)
         end;
       _ ->
         exception(error, {over_lambda_fun_argument_limit, Arity})
     end,
   mk_result(LambdaC, LambdaS).
 
-make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, FileDescr) ->
+make_fun_h1(Mod, Args, Servers, Vars, Body, Cenv, Senv, Creator, LambdaS, FileDescr, Options) ->
   {Ce, Se, SAs} = register_new_environments(Args, Vars, Cenv, Senv),
   NSvs = validate_servers(Servers),
   Fd = validate_file_descriptor(NSvs#svs.monitor, Creator, FileDescr),
-  Ret = eval_expr(Body, Mod, Ce, Se, NSvs, Fd),
-  cuter_log:log_evaluated_closure(Fd, LambdaS, SAs, get_symbolic(Ret)),
+  Ret = eval_expr(Body, Mod, Ce, Se, NSvs, Fd, Options),
+  conditional_log(fun cuter_log:log_evaluated_closure/4, [Fd, LambdaS, SAs, get_symbolic(Ret)], Options),
   Ret.
 
 register_new_environments([], _Vars, Cenv, Senv) ->
@@ -1413,7 +1444,7 @@ register_new_environments(Args, Vars, Cenv, Senv) ->
 
 %% Creates a closure from an MFA (emulates the behaviour
 %% of erlang:make_fun/3) 
-make_fun(Mod, Func, Arity, Servers, Fd) ->
+make_fun(Mod, Func, Arity, Servers, Fd, Options) ->
   Creator = self(),
   LambdaS = cuter_symbolic:fresh_lambda(Arity, Fd),
   add_to_created_closure(LambdaS),
@@ -1421,94 +1452,94 @@ make_fun(Mod, Func, Arity, Servers, Fd) ->
     case Arity of
       0 ->
         fun() ->
-          make_fun_h(Mod, Func, [], Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, [], Servers, Creator, LambdaS, Fd, Options)
         end;
       1 ->
         fun(A) ->
           Args = [A],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       2 ->
         fun(A, B) ->
           Args = [A, B],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       3 ->
         fun(A, B, C) ->
           Args = [A, B, C],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       4 ->
         fun(A, B, C, D) ->
           Args = [A, B, C, D],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       5 ->
         fun(A, B, C, D, E) ->
           Args = [A, B, C, D, E],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       6 ->
         fun(A, B, C, D, E, F) ->
           Args = [A, B, C, D, E, F],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       7 ->
         fun(A, B, C, D, E, F, G) ->
           Args = [A, B, C, D, E, F, G],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       8 ->
         fun(A, B, C, D, E, F, G, H) ->
           Args = [A, B, C, D, E, F, G, H],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       9 ->
         fun(A, B, C, D, E, F, G, H, I) ->
           Args = [A, B, C, D, E, F, G, H, I],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       10 ->
         fun(A, B, C, D, E, F, G, H, I, J) ->
           Args = [A, B, C, D, E, F, G, H, I, J],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       11 ->
         fun(A, B, C, D, E, F, G, H, I, J, K) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       12 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       13 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L, M) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L, M],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       14 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L, M, N) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L, M, N],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       15 ->
         fun(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) ->
           Args = [A, B, C, D, E, F, G, H, I, J, K, L, M, N, O],
-          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd)
+          make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, Fd, Options)
         end;
       _ ->
         exception(error, {over_lambda_fun_argument_limit, Arity})
     end,
   mk_result(LambdaC, LambdaS).
 
-make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, FileDescr) ->
+make_fun_h(Mod, Func, Args, Servers, Creator, LambdaS, FileDescr, Options) ->
   {CAs, SAs} = unzip_args(Args), %% If Args =:= [] then unzip_args([]) will return {[], []}
   NSvs = validate_servers(Servers),
   Fd = validate_file_descriptor(NSvs#svs.monitor, Creator, FileDescr),
-  Ret = eval({named, Mod, Func}, CAs, SAs, external, NSvs, Fd),
-  cuter_log:log_evaluated_closure(Fd, LambdaS, SAs, get_symbolic(Ret)),
+  Ret = eval({named, Mod, Func}, CAs, SAs, external, NSvs, Fd, Options),
+  conditional_log(fun cuter_log:log_evaluated_closure/4, [Fd, LambdaS, SAs, get_symbolic(Ret)], Options),
   Ret.
 
 %% --------------------------------------------------------
@@ -1947,3 +1978,11 @@ log_bistr_type_mismatch(Cv, Sv, Type, Fd) ->
           throw({unknown_bitstr_type, Type})
       end
   end.
+
+conditional_log(LogFun, Args, Options) ->
+  case maps:get(constraintLogging, Options) of
+    true ->
+      apply(LogFun, Args);
+    false ->
+      ok
+  end.
diff --git a/src/cuter_graphs.erl b/src/cuter_graphs.erl
new file mode 100644
index 00000000..ace02d66
--- /dev/null
+++ b/src/cuter_graphs.erl
@@ -0,0 +1,394 @@
+-module(cuter_graphs).
+-export([make_graph_from_children/2, children/2, list_contains/2, calculate_dag_callgraph/1]).
+-export_type([graph/0, graph_node/0]).
+%debugging
+-export([print_graph/1, report_callgraphs/1]).
+
+
+% ================
+% types for graphs
+% ================
+
+-type graph() :: dict:dict().
+-type graph_node() :: mfa() 
+		    | {node, mfa()} 
+		    | {scc, [mfa()]}.
+
+
+%% =====================================================
+%% Graph implementation. Each graph is a dictionary with
+%%  nodes as keys and their list of neighbours as values
+%% =====================================================
+
+%% Creates an empty dict representing a graph.
+new_graph() ->
+  dict:new().
+
+%% Adds a new node with no neighbours to a graph.
+add_node(Node, Graph) ->
+  dict:store(Node, [], Graph).
+
+%% Adds an edge to a graph.
+add_edge({Node1, Node2}, Graph) ->
+  %% Add Node2 into the list of neighbours of Node1
+  dict:store(Node1, [Node2|element(2, dict:find(Node1, Graph))], Graph).
+
+%% Adds a node along with its neighbours in a graph.
+add_node_with_children(Node, Children, Graph) ->
+  NewGraph = add_node(Node, Graph),
+  lists:foldl(fun(A, B) -> add_edge({Node, A}, B) end, NewGraph, Children).
+
+%% Given a list of nodes and a list of neighbours per node, it returns a graph.
+-spec make_graph_from_children([node()], [[node()]]) -> graph().
+make_graph_from_children(Nodes, Children) ->
+  G = lists:foldl(fun add_node/2, new_graph(), Nodes),
+  lists:foldl(fun({Node, Ch}, B) -> dict:store(Node, Ch, B) end, G, lists:zip(Nodes, Children)).
+
+%% Returns the neighbour list of a node in a graph.
+-spec children(graph_node(), graph()) -> [graph_node()].
+children(Node, Graph) ->
+  {ok, C} = dict:find(Node, Graph),
+  C.
+
+%% Returns all the nodes of a graph.
+get_nodes(Graph) ->
+  dict:fetch_keys(Graph).
+
+%% Checks if a node is contained in a graph.
+has_node(Node, Graph) ->
+  dict:is_key(Node, Graph).
+
+
+%% =====================================================
+%% Logic for finding sccs. Implemented as a DFS search
+%% with a visited set.
+%% =====================================================
+
+%% Returns a list of sccs in a graph.
+scc_nodes(EntryPoint, Graph) ->
+  {Sccd, _, _} = scc_nodes(EntryPoint, Graph, sets:new(), sets:new()),
+  Sccd.
+
+scc_nodes(Node, Graph, Visited, Ignored) ->
+  %% Get the children of the node.
+  C = children(Node, Graph),
+  %% Filter out the ones that have been visited or are ignored.
+  TC = [Y || Y <- C, not (sets:is_element(Y, Visited) or sets:is_element(Node, Ignored))],
+  %% Call self for every child.
+  {ChildrenSccd, ChildrenActiveSccd, VisitedBelow} = scc_nodes_children(TC, Graph, sets:add_element(Node, Visited), Ignored),
+  %% An active scc is a detected scc that hasn't been
+  %% completed yet when backtracking
+  ActiveSccd = lists:filter(fun(X) -> sets:is_element(X, Visited) end, C),
+  {Sccs, ActiveSccs} = update_active_sccs(Node, ActiveSccd, ChildrenSccd, ChildrenActiveSccd),
+  {Sccs, ActiveSccs, sets:add_element(Node, VisitedBelow)}.
+
+scc_nodes_children(C, G, V, I) ->
+  scc_nodes_children(C, G, V, I, [], [], sets:new()).
+
+scc_nodes_children([], _, _, _, SccAcc, ActiveSccAcc, VisitedAcc) ->
+  {SccAcc, ActiveSccAcc, VisitedAcc};
+scc_nodes_children([Ch|C], G, V, I, SccAcc, ActiveSccAcc, VisitedAcc) ->
+  {Scc, ActiveScc, VisitedBelow} = scc_nodes(Ch, G, V, I),
+  scc_nodes_children(C, G, V, sets:union([I, VisitedBelow]), lists:append([SccAcc, Scc]), lists:append([ActiveSccAcc,  ActiveScc]), sets:union([VisitedAcc, VisitedBelow])).
+
+update_active_sccs(Node, ActiveSccd, ChildrenSccd, ChildrenActiveSccd) ->
+  ActiveSccd1 = create_new_sccs(ActiveSccd, ChildrenActiveSccd),
+  {Sccs1, ActiveSccd2} = update_all_sccs(Node, ActiveSccd1),
+  {lists:append([Sccs1, ChildrenSccd]), ActiveSccd2}.
+
+create_new_sccs([], Acc) ->
+  Acc;
+create_new_sccs([H|T], Acc) ->
+  [{H,[]}|create_new_sccs(T, Acc)].
+
+update_all_sccs(Node, ActiveSccd) ->
+  update_all_sccs(Node, ActiveSccd, [], []).
+
+update_all_sccs(_, [], ActiveAcc, SccsAcc) ->
+  {SccsAcc, ActiveAcc};
+update_all_sccs(Node, [{First, List}|T], ActiveAcc, SccsAcc) ->
+  case First of
+    Node ->
+      SccsAcc1 = [[Node|List]|SccsAcc],
+      ActiveAcc1 = ActiveAcc;
+    _ ->
+      SccsAcc1 = SccsAcc,
+      ActiveAcc1 = [{First, [Node|List]}|ActiveAcc]
+  end,
+  update_all_sccs(Node, T, ActiveAcc1, SccsAcc1).
+
+
+%% =================================================================
+%% Logic for merging overlapping sccs.
+%% Overlapping sccs are sccs that have at least one common node.
+%% Each scc is a list of nodes, so we have to find all lists with
+%% common elements and merge them.
+%% =================================================================
+
+%% Sccs are lists of nodes.
+%% If two sccs contain at least one commone element are merged into one list.
+merge_sccs(Sccs) ->
+  %% Make a helper graph.
+  G = make_help_graph(Sccs),
+  %% Merged sccs are the connected components of the helper graph.
+  connected_components(G).
+
+%% Creates the helper graph for merging the sccs.
+-spec make_help_graph([[graph_node()]]) -> dict:dict().
+make_help_graph(Sccs) ->
+  %% Initialize a graph.
+  G = dict:new(),
+  %% Add each scc to the graph.
+  lists:foldl(fun put_scc/2, G, Sccs).
+
+%% Adds a scc to a helper graph.
+-spec put_scc([graph_node()], dict:dict()) -> dict:dict().
+put_scc(Scc, Graph) -> put_scc(nonode, Scc, Graph).
+
+%% If we don't have other nodes to add, return the graph.
+put_scc(_, [], Graph) -> Graph;
+put_scc(Prev, [N|Ns], Graph) ->
+  %% If the node is not already in the graph, add it.
+  Graph1 = case dict:is_key(N, Graph) of
+	     true ->
+	       Graph;
+	     false ->
+	       dict:store(N, [], Graph)
+	   end,
+  %% Connect the previous node with the current one bidirectionally.
+  Graph2 = case Prev of
+	     nonode ->
+	       Graph1;
+	     _ ->
+	       G = dict:append_list(Prev, [N], Graph1),
+	       dict:append_list(N, [Prev], G)
+	   end,
+  put_scc(N, Ns, Graph2).
+
+%% Returns the connected components of a graph.
+connected_components(G) ->
+  connected_components(G, []).
+
+connected_components(G, Acc) ->
+  %% If the graph is empty, we have found all connected components.
+  case dict:is_empty(G) of
+    true ->
+      Acc;
+    false ->
+      %% Else, get one connected component.
+      C = connected_component(G),
+      %% Remove the whole component from G.
+      G1 = remove_nodes(C, G),
+      %% Find the rest connected components.
+      connected_components(G1, [C|Acc])
+  end.
+
+connected_component(G) ->
+  %% To find one connected component, fetch a random node from the graph
+  %% and find everything that can be reached from that node.
+  connected_component(hd(dict:fetch_keys(G)), sets:new(), G).
+
+%% Finds the connected component of Graph
+%% which contains the node Node given that we have
+%% visited Visited nodes of this component already
+connected_component(Node, Visited, Graph) ->
+  %% Get the neighbours of this Node.
+  {ok, Children} = dict:find(Node, Graph),
+  %% Add them to the visited set.
+  Visited1 = sets:add_element(Node, Visited),
+  %% Call self for each child through connected_component_children/3.
+  connected_component_children(Children, Visited1, Graph).
+
+%% Calls connected_component/3 for each of the nodes
+%% in a list if they haven't alreadybeen visited.
+%% Returns all the nodes that have been visited by
+%% this procedure.
+connected_component_children([], Visited, _) -> Visited;
+connected_component_children([C|Cs], Visited, Graph) ->
+  %% If node C has not been visited.
+  case sets:is_element(C, Visited) of
+    false ->
+      %% Find the connected component containing this node.
+      Visited1 = connected_component(C, Visited, Graph);
+    true ->
+      Visited1 = Visited
+  end,
+  connected_component_children(Cs, Visited1, Graph).
+
+%% Removes all nodes in list C from graph G.
+remove_nodes(C, G) ->
+  lists:foldl(fun dict:erase/2, G, sets:to_list(C)).
+
+
+%% ==================================================
+%% Logic for making a new graph merging sccd nodes.
+%% ==================================================
+
+remake_graph(EntryPoint, Graph) ->
+  Sccs = merge_sccs(scc_nodes(EntryPoint, Graph)),
+  SccNodes = [{scc, sets:to_list(X)} || X <- Sccs],
+  AllSccdNodes = sets:union(Sccs),
+  Children = find_children([A || {scc, A} <- SccNodes], Graph),
+  NewNodes = [{node, X} || X <- get_nodes(Graph), not sets:is_element(X, AllSccdNodes)],
+  NewChildren = [update_children(children(Y, Graph), AllSccdNodes, Sccs, SccNodes) || {node, Y} <- NewNodes],
+  SccChildren = [update_children(Z, AllSccdNodes, Sccs, SccNodes) || Z <- Children],
+  Nodes = lists:append(NewNodes, SccNodes),
+  ChildrenPerNodeTemp = [sets:to_list(sets:from_list(W)) || W <- lists:append(NewChildren, SccChildren)],
+  ChildrenPerNode = [try_remove(B, C) || {B, C} <- lists:zip(Nodes, ChildrenPerNodeTemp)],
+  make_graph_from_children(Nodes, ChildrenPerNode).  
+
+find_children(Sccs, Graph) ->
+  find_children(Sccs, Graph, []).
+
+find_children([], _, Acc) -> lists:reverse(Acc);
+find_children([C|Cs], Graph, Acc) ->
+  find_children(Cs, Graph, [lists:append([children(X, Graph) || X <- C])|Acc]).
+
+update_children(Children, AllSccdNodes, Sccs, SccsAsLists) ->
+  update_children(Children, AllSccdNodes, Sccs, SccsAsLists, []).
+
+update_children([], _, _, _, Acc) -> Acc;
+update_children([C|Cs], AllSccs, Sccs, SccsAsLists, Acc) -> 
+  case sets:is_element(C, AllSccs) of
+    true ->
+      update_children(Cs, AllSccs, Sccs, SccsAsLists, [which_scc(C, Sccs, SccsAsLists)|Acc]);
+    false ->
+      update_children(Cs, AllSccs, Sccs, SccsAsLists, [{node, C}|Acc])
+  end.
+
+which_scc(_, [], _) -> error('scc not found');
+which_scc(Node, [C|Cs], [CL|CLs]) ->
+  case sets:is_element(Node, C) of
+    true ->
+      CL;
+    false ->
+      which_scc(Node, Cs, CLs)
+  end.
+
+try_remove(Node, Children) ->
+  try_remove(Node, Children, []).
+
+try_remove(_, [], Acc) -> Acc;
+try_remove(Node, [C|Cs], Acc) -> 
+  case Node == C of
+    true ->
+      try_remove(Node, Cs, Acc);
+    false ->
+      try_remove(Node, Cs, [C|Acc])
+  end.
+
+
+%% ===========================================================
+%% Logic for calculating a callgraph and merging all functions 
+%% having a cyclic dependency onto a new node.
+%% ===========================================================
+
+%% First calculates the callgraph.
+%% Then it replaces all sccs with single nodes,
+%% merging sccs with common functions.
+%% Last it finds the new entry point which may be part of a scc.
+%% Returns the processed callgraph, all functions belonging to the callgraph in a set
+%% and the new entry point.
+-spec calculate_dag_callgraph(mfa()) -> {graph(), sets:set(), graph_node()}.
+calculate_dag_callgraph(EntryPoint) ->
+  Original = calculate_callgraph(EntryPoint),
+  CallGraph = remake_graph(EntryPoint, Original),
+  NewEntryPoint = find_entry_point(EntryPoint, CallGraph),
+  {CallGraph, sets:from_list(dict:fetch_keys(Original)), NewEntryPoint}.
+
+%% Finds the new entry point of the graph
+find_entry_point(EntryPoint, Graph) ->
+  case has_node({node, EntryPoint}, Graph) of
+    true ->
+      %% If entry point is just a node, return it.
+      {node, EntryPoint};
+    false ->
+      %% Else return the first scc that contains the entry point.
+      %% Only one scc will contain it, since if it belonge to many,
+      %% they would have been merged.
+      {scc, hd([C || {scc, C} <- get_nodes(Graph), list_contains(EntryPoint, C)])}
+  end.
+
+%% Calculates the callgraph produced by the
+%% visibly reachable mfas from an entry point.
+calculate_callgraph(EntryPoint) ->
+  %% Start the xref server.
+  xref:start(s),
+  %% Add all modules reachable by the entry point
+  %% in the xref server.
+  _FoundModules = add_modules_rec(EntryPoint),
+  %% Make the callgraph from the gathered modules.
+  CallGraph = make_callgraph(EntryPoint, new_graph()),
+  %% Stop the xref server.
+  xref:stop(s),
+  CallGraph.
+
+%% Adds to the xref server the module of the argument mfa.
+%% Then it recursively adds the modules of the functions called by the mfa.
+add_modules_rec(MFA) ->
+  add_modules_rec(MFA, sets:new(), sets:new()).
+
+add_modules_rec({M, _F, _A}=MFA, Found, FoundNodes) ->
+  %% Function used to filter edges pointing to compiler generated functions (eg. from list comprehensions).
+  Valid = fun({_, {M1, F1, _A1}}) ->
+	      %% The compiler generated function name starts with char '$'.
+	      hd(atom_to_list(M1)) =/= 36 andalso hd(atom_to_list(F1)) =/= 36 
+	  end,
+  %% If we haven't seen the mfa's module yet, add it to the xref server and the Found set.
+  NewFound = case sets:is_element(M, Found) of
+	       false ->
+		 xref:add_module(s, code:which(M)),
+		 sets:add_element(M, Found);
+	       true ->
+		 Found
+	     end,
+  %% Get the outward edges from our mfa to other functions.
+  %% To do this, we make a query to the xref server starting with
+  %% 'E' to fetch edges and use | <mfa> to specify those that start with our mfa.
+  {ok, Edges1} = xref:q(s, lists:concat(["E | ", mfa_to_str(MFA)])),
+  %% Filter the edges to compiler generated functions.
+  Edges = lists:filter(Valid, Edges1),
+  %% Add the current mfa to FoundNodes set.
+  NewFoundNodes = sets:add_element(MFA, FoundNodes),
+  lists:foldl(fun(X, Y) -> add_modules_rec(X, Y, NewFoundNodes) end, NewFound, [N2 || {_N1, N2} <- Edges, not sets:is_element(N2, FoundNodes)]).
+
+make_callgraph(MFA, Graph) ->
+  case has_node(MFA, Graph) of
+    true -> Graph;
+    false ->
+      Valid = fun({_, {M1, F1, _A}}) -> hd(atom_to_list(M1)) =/= 36 andalso hd(atom_to_list(F1)) =/= 36 end,
+      {ok, ChildEdges1} = xref:q(s, lists:concat(["E | ", mfa_to_str(MFA)])),
+      ChildEdges = lists:filter(Valid, ChildEdges1),
+      Children = [B || {_A,B} <- ChildEdges],
+      NewGraph = add_node_with_children(MFA, Children, Graph),
+      lists:foldl(fun make_callgraph/2, NewGraph, Children)
+  end.
+
+-spec list_contains(any(), [any()]) -> boolean().
+list_contains(_, []) -> false;
+list_contains(X, [H|_T]) when X == H -> true;
+list_contains(X, [_H|T]) -> list_contains(X, T). 
+
+-spec mfa_to_str(mfa()) -> string().
+mfa_to_str({M, F, A}) ->
+  lists:concat([atom_to_list(M), ":", atom_to_list(F), "/", lists:flatten(io_lib:format("~p", [A]))]).
+
+		       
+% =============
+% for debugging
+% =============
+
+-spec print_graph(graph()) -> ok.
+print_graph(Graph) ->
+  lists:foreach(fun(A) -> io:format("~p: ~p;~n", [A, children(A, Graph)]) end, get_nodes(Graph)).
+
+-spec report_callgraphs(mfa()) -> ok.
+report_callgraphs(EntryPoint) ->
+  Original = calculate_callgraph(EntryPoint),
+  io:format("Original callgraph:~n"),
+  graphs:print_graph(Original),
+  CallGraph = remake_graph(EntryPoint, Original),
+  NewEntryPoint = find_entry_point(EntryPoint, CallGraph),
+  io:format("Final callgraph:~n"),
+  graphs:print_graph(CallGraph),
+  io:format("New Entry Point: ~p ~n", [NewEntryPoint]).
diff --git a/src/cuter_log.erl b/src/cuter_log.erl
index 146fb50f..850641f7 100644
--- a/src/cuter_log.erl
+++ b/src/cuter_log.erl
@@ -331,10 +331,10 @@ log(Fd, OpCode, TagID, Data) ->
     N when is_integer(N), N > 0 ->
       IsConstraint = is_constraint(OpCode),
       try cuter_serial:to_log_entry(OpCode, Data, IsConstraint, TagID) of
-        Jdata ->
-          write_data(Fd, Jdata)
+	Jdata ->
+	  write_data(Fd, Jdata)
       catch
-        throw:{unsupported_term, _} -> ok
+	throw:{unsupported_term, _} -> ok
       end
   end.
 -else.
diff --git a/src/cuter_maybe_error_annotation.erl b/src/cuter_maybe_error_annotation.erl
new file mode 100644
index 00000000..c675f0e3
--- /dev/null
+++ b/src/cuter_maybe_error_annotation.erl
@@ -0,0 +1,619 @@
+-module(cuter_maybe_error_annotation).
+-export([preprocess/3, get_force_constraint_logging/1, get_maybe_error_bin/2, get_maybe_error_bin_anno/2, get_distrust_type_dependent/1]).
+-export_type([maybe_error/0, symbol_table/0]).
+
+%% ==========
+%% Used types
+%% ==========
+
+-type maybe_error() :: false | type_dependent | true.
+-type symbol_table() :: dict:dict().
+
+%% ============================
+%% Annotating a callgraph logic
+%% ============================
+
+%% Creates a symbol table from a type symbol table.
+%% The symbol table we need here is a dictionary with
+%% variables or functions as keys and whether they are safe
+%% or not as values. The type symbol table just has type information
+%% for various symbols.
+st_from_tsm() ->
+  %% Using the original_tsm() we will store each of those functions
+  %% as 'type_dependent' in the symbol table.
+  lists:foldl(
+    fun({Fun, _}, ST) ->
+        dict:store(Fun, {type_dependent, 'fun'}, ST)
+    end,
+    dict:new(),
+    dict:to_list(cuter_type_dependent_functions:original_tsm())
+   ).
+
+%% Main entry point of the analysis.
+%% Arguments:
+%% - EntryPoint: The entry point of CutEr analysis
+%% - FunctionAsts: Dictionary from Mfas to ASTs.
+%% - Graph: The updated from cuter_graphs callgraph.
+annotate_callgraph(EntryPoint, FunctionAsts, Graph) ->
+  {Annotated, _} = annotate_callgraph(EntryPoint, FunctionAsts, Graph, st_from_tsm()),
+  Annotated.
+
+%% Annotates a node in the callgraph.
+annotate_callgraph(Node, FunctionAsts, Graph, ST) ->
+  %% First annotate its children.
+  {FunctionAsts1, ST1} = lists:foldl(fun(A, {Funs, SmT}) -> annotate_callgraph(A, Funs, Graph, SmT) end, {FunctionAsts, ST}, cuter_graphs:children(Node, Graph)),
+  %% Distinguish between just functions and SCCs.
+  case Node of
+    {node, Name} ->
+      %% If it is just a function, annotate it.
+      {ok, PrevAST} = dict:find(Name, FunctionAsts1),
+      {NewAST, _C, _SelfReffed} = annotate_maybe_error(PrevAST, ST1, sets:new(), element(1, Name)),
+      {dict:store(Name, NewAST, FunctionAsts1), dict:store(Name, {get_maybe_error(NewAST), 'fun'}, ST1)};
+    {scc, Scc} ->
+      %% If it is an SCC, do a fix-point on it.
+      scc_annotation(Scc, FunctionAsts1, ST1)
+  end.
+
+%% SCC annotation fix-point.
+scc_annotation(Scc, FunctionAsts, ST) ->
+  %% Gather the ASTs of the functions in the SCC.
+  ASTS = [element(2, dict:find(A, FunctionAsts)) || A <- Scc],
+  SccSet = sets:from_list(Scc),
+  %% Do the actual fix-point and return the ASTs and the updated symbol table.
+  {NewASTS, NewST} = scc_annotation_helper(Scc, ASTS, ST, SccSet),
+  {
+   lists:foldl(
+     fun({Name, AST}, Y) -> dict:store(Name, AST, Y) end,
+     FunctionAsts, 
+     lists:zip(Scc, NewASTS)
+    ),
+   NewST
+  }.
+
+%% Performs the fix-point computation for an SCC.
+scc_annotation_helper(Scc, ASTS, ST, SccSet) ->
+  %% Do a pass to all functions in the SCC.
+  {NewASTS, ST1, C} = scc_pass(Scc, ASTS, ST, SccSet),
+  %% Check if some annotation has changed. If not, we are done, else, continue passing.
+  case C of
+    false -> {NewASTS, ST1};
+    true -> scc_annotation_helper(Scc, NewASTS, ST1, SccSet)
+  end.
+
+%% Does a pass on the SCC functions.
+scc_pass(Scc, ASTS, ST, SccSet) ->
+  scc_pass_helper(SccSet, Scc, ASTS, ST, [], false).
+
+scc_pass_helper(_, [], _, ST, AccAST, AccC) -> {lists:reverse(AccAST), ST, AccC};
+scc_pass_helper(SccSet, [Name|Names], [AST|ASTS], ST, AccAST, AccC) ->
+  {NewAST, C, IgnoredFound} = annotate_maybe_error(AST, ST, SccSet, element(1, Name)),
+  ST1 = dict:store(Name, {get_maybe_error(NewAST), 'fun'}, ST),
+  scc_pass_helper(SccSet, Names, ASTS, ST1, [NewAST|AccAST], AccC or C or IgnoredFound).
+
+
+%% ===========================
+%% Annotating a function logic
+%% ===========================
+
+%% Updates the 'maybe_error' annotation of a node T.
+update_ann(T, Maybe_Error) ->
+  Anno = cerl:get_ann(T),
+  cerl:set_ann(T, update_ann(Anno, Maybe_Error, [], false)).
+
+%% Updates the 'maybe_error' annotation in a list of annotations.
+update_ann([], Maybe_Error, Acc, false) -> [{maybe_error, Maybe_Error}|Acc];
+update_ann([], _, Acc, true) -> Acc; 
+update_ann([{maybe_error, _}|T], Maybe_Error, Acc, _) -> update_ann(T, Maybe_Error, [{maybe_error, Maybe_Error}|Acc], true); 
+update_ann([H|T], Maybe_Error, Acc, Found) -> update_ann(T, Maybe_Error, [H|Acc], Found).
+
+%% Adds the 'force_constraint_logging' annotation in node Tree.
+add_force_constraint_logging(Tree) ->
+  Anno = cerl:get_ann(Tree),
+  case cuter_graphs:list_contains({force_constraint_logging, true}, Anno) of
+    true -> Tree;
+    false -> cerl:add_ann([{force_constraint_logging, true}], Tree)
+  end.
+
+%% Adds the 'distrust_type_dependent' annotation in a node Tree.
+add_distrust_type_dependent(Tree) ->
+  Anno = cerl:get_ann(Tree),
+  case cuter_graphs:list_contains({distrust_type_dependent, true}, Anno) of
+    true -> Tree;
+    false -> cerl:add_ann([{distrust_type_dependent, true}], Tree)
+  end.
+
+%% Adds variables Vars with annotations Flags to the symbol table SM.
+put_vars(Vars, Flags, SM) ->
+  lists:foldl(fun({Var, Flag}, B) -> dict:store(cerl:var_name(Var), Flag, B) end, SM, lists:zip(Vars, Flags)).
+
+%% Add variables to the symbol table given their names directly and not var cerl nodes.
+put_vars_by_name(Vars, Flags, SM) ->
+  lists:foldl(fun({Var, Flag}, B) -> dict:store(Var, Flag, B) end, SM, lists:zip(Vars, Flags)).
+
+%% ================
+%% Annotation logic
+%% ================
+
+%% Entrypoint of the annotation of a single function.
+%% Arguments:
+%% - AST: The AST of the function.
+%% - ST: The symbol table with symbols as keys and 'maybe_error' annotations as values.
+%% - Ignored: Funtions belonging to the same SCC.
+%% - Mod: The module that the current function is defined in.
+%% This function is just a wrapper for annotate_maybe_error/6
+annotate_maybe_error(AST, ST, Ignored, Mod) ->
+  {NewAST, C, _, IgnoredCall, _} = annotate_maybe_error(AST, ST, false, Ignored, sets:new(), Mod),
+  {NewAST, C, IgnoredCall}.
+
+%% Performs the AST annotation.
+%% It has the same arguments as annotate_maybe_error/4 with 2 additional ones:
+%% - Force: Whether we are in a state that evaluation should be forced.
+%% - LetrecIgnored: letrec nodes introduce closures which can define their own SCCs.
+%%   In the simple case where we have a list comprehension, a recursive closure is defined
+%%   which is trivially an SCC. Thus we need to do an inner fix-point computation
+%%   same as the cross function one handling the SCCs in the callgraph.
+%%   This argument contains the rest closures under the same letrec node that
+%%   belong to the same SCC.
+annotate_maybe_error(Tree, SM, Force, Ignored, LetrecIgnored, Mod) ->
+  CurMaybe_Error = get_maybe_error(Tree),
+  %% We distinguish the type of the node we are annotating.
+  %% Most nodes just call this function recursively in their children
+  %% and combine their results to return.
+  case cerl:type(Tree) of
+    'apply' ->
+      annotate_maybe_error_apply(Tree, SM, Force, Ignored, LetrecIgnored, Mod, CurMaybe_Error);
+    call ->
+      annotate_maybe_error_call(Tree, SM, Force, Ignored, LetrecIgnored, Mod, CurMaybe_Error);
+    'case' ->
+      %% We have a case node to annotate. First, annotate the clauses.
+      {Clauses, C1, Found1, IgnoreFound1, LetrecFound1} = annotate_maybe_error_all(cerl:case_clauses(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      ClausesError1 = get_all_maybe_error(Clauses),
+      %% Maybe error annotation should disregard unreachable clauses.
+      ClausesError =
+        case unreachable_clauses(Clauses) of
+          true -> maybe_error_or([ClausesError1, type_dependent]);
+          false -> ClausesError1
+        end,
+      %% Annotate the argument.
+      {Arg, C2, Found2, IgnoreFound2, LetrecFound2} = 
+        case ClausesError of
+          true -> annotate_maybe_error(cerl:case_arg(Tree), SM, true, Ignored, LetrecIgnored, Mod);
+          type_dependent -> annotate_maybe_error(cerl:case_arg(Tree), SM, Force, Ignored, LetrecIgnored, Mod);
+          false -> annotate_maybe_error(cerl:case_arg(Tree), SM, Force, Ignored, LetrecIgnored, Mod)
+        end,
+      %% Combine everything to produce the maybe_error annotation of this node.
+      NewMaybe_Error = maybe_error_or([get_maybe_error(Arg), ClausesError]),
+      {cerl:update_c_case(update_ann(Tree, NewMaybe_Error), Arg, Clauses), C1 or C2, sets:union([Found1, Found2]), IgnoreFound1 or IgnoreFound2, sets:union([LetrecFound1, LetrecFound2])};
+    clause ->
+      {Pats, C1, Found1, SM1} = annotate_maybe_error_pattern_all(cerl:clause_pats(Tree), SM, Force),
+      IgnoreFound1 = false,
+      {Guard, C2, Found2, IgnoreFound2, LetrecFound2} = annotate_maybe_error(cerl:clause_guard(Tree), SM1, Force, Ignored, LetrecIgnored, Mod),
+      {Body, C3, Found3, IgnoreFound3, LetrecFound3} = annotate_maybe_error(cerl:clause_body(Tree), SM1, Force, Ignored, LetrecIgnored, Mod),
+      NewIgnoreFound = IgnoreFound1 or IgnoreFound2 or IgnoreFound3,
+      NewLetrecFound = sets:union([LetrecFound2, LetrecFound3]),
+      NewMaybe_Error = maybe_error_or([get_maybe_error(Body), get_all_maybe_error(Pats), get_maybe_error(Guard)]),
+      {cerl:update_c_clause(update_ann(Tree, NewMaybe_Error), Pats, Guard, Body), C1 or C2 or C3, sets:union([Found1, Found2, Found3]), NewIgnoreFound, NewLetrecFound};
+    cons ->
+      {Hd, C1, Found1, IgnoreFound1, LetrecFound1} = annotate_maybe_error(cerl:cons_hd(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      {Tl, C2, Found2, IgnoreFound2, LetrecFound2} = annotate_maybe_error(cerl:cons_tl(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      NewIgnoreFound = IgnoreFound1 or IgnoreFound2,
+      NewLetrecFound = sets:union([LetrecFound1, LetrecFound2]),
+      NewMaybe_Error = maybe_error_or([get_maybe_error(Hd), get_maybe_error(Tl)]),
+      {cerl:update_c_cons_skel(update_ann(Tree, NewMaybe_Error), Hd, Tl), C1 or C2, sets:union([Found1, Found2]), NewIgnoreFound, NewLetrecFound};
+    'fun' ->
+      %% For function nodes we also have to add their arguments to the symbol table.
+      Flags = make_fun_flags(cerl:fun_vars(Tree)),
+      SM1 = put_vars(cerl:fun_vars(Tree), Flags, SM),
+      {Vars, C1, Found1, IgnoreFound1, LetrecFound1} = annotate_maybe_error_all(cerl:fun_vars(Tree), SM1, Force, Ignored, LetrecIgnored, Mod),
+      {Body, C2, Found2, IgnoreFound2, LetrecFound2} = annotate_maybe_error(cerl:fun_body(Tree), SM1, Force, Ignored, LetrecIgnored, Mod),
+      NewMaybe_Error = maybe_error_or([get_maybe_error(Body), get_all_maybe_error(Vars)]),
+      {cerl:update_c_fun(update_ann(Tree, NewMaybe_Error), Vars, Body), C1 or C2, sets:union([Found1, Found2]), IgnoreFound1 or IgnoreFound2, sets:union([LetrecFound1, LetrecFound2])};
+    'let' ->
+      %% For let nodes we also have to add the newly created variables to the symbol table.
+      {Arg, C2, Found1, IgnoreFound1, LetrecFound1} = annotate_maybe_error(cerl:let_arg(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      SM1 = put_vars(cerl:let_vars(Tree), get_arg_maybe_errors(Arg), SM),
+      {Vars, C1, Found2, IgnoreFound2, LetrecFound2} = annotate_maybe_error_all(cerl:let_vars(Tree), SM1, Force, Ignored, LetrecIgnored, Mod),
+      {Body, C3, Found3, IgnoreFound3, LetrecFound3} = annotate_maybe_error(cerl:let_body(Tree), SM1, Force, Ignored, LetrecIgnored, Mod),
+      Tree1 =
+        case vars_in_set(cerl:let_vars(Tree), Found3) of
+          true ->
+            add_force_constraint_logging(Tree);
+          false ->
+            Tree
+        end,  
+      NewMaybe_Error = maybe_error_or([get_all_maybe_error(Vars), get_maybe_error(Arg), get_maybe_error(Body)]),
+      NewIgnoreFound = IgnoreFound1 or IgnoreFound2 or IgnoreFound3,
+      NewLetrecFound = sets:union([LetrecFound1, LetrecFound2, LetrecFound3]),
+      {cerl:update_c_let(update_ann(Tree1, NewMaybe_Error), Vars, Arg, Body), C1 or C2 or C3, sets:union([Found1, Found2, Found3]), NewIgnoreFound, NewLetrecFound};
+    letrec ->
+      annotate_maybe_error_letrec(Tree, SM, Force, Ignored, LetrecIgnored, Mod, CurMaybe_Error);
+    literal ->
+      {update_ann(Tree, false), true == CurMaybe_Error, sets:new(), false, sets:new()};
+    primop ->
+      %% Primops are unsafe by default.
+      {update_ann(Tree, true), false == CurMaybe_Error, sets:new(), false, sets:new()};
+    seq ->
+      {Arg, C1, Found1, IgnoreFound1, LetrecFound1} = annotate_maybe_error(cerl:seq_arg(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      {Body, C2, Found2, IgnoreFound2, LetrecFound2} = annotate_maybe_error(cerl:seq_body(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      NewIgnoreFound = IgnoreFound1 or IgnoreFound2,
+      NewLetrecFound = sets:union([LetrecFound1, LetrecFound2]),
+      NewMaybe_Error = maybe_error_or([get_maybe_error(Arg), get_maybe_error(Body)]),
+      {cerl:update_c_seq(update_ann(Tree, NewMaybe_Error), Arg, Body), C1 or C2, sets:union([Found1, Found2]), NewIgnoreFound, NewLetrecFound};
+    'try' ->
+      %% Since we don't categorize the errors produced, we don't let them exist
+      %% even in a try construct. If something is unsafe, the whole try is unsafe.
+      {Arg, C1, Found1, IgnoreFound1, LetrecFound1} = annotate_maybe_error(cerl:try_arg(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      {Vars, C2, Found2, IgnoreFound2, LetrecFound2} = annotate_maybe_error_all(cerl:try_vars(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      {Body, C3, Found3, IgnoreFound3, LetrecFound3} = annotate_maybe_error(cerl:try_body(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      {Evars, C4, Found4, IgnoreFound4, LetrecFound4} = annotate_maybe_error_all(cerl:try_evars(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      {Handler, C5, Found5, IgnoreFound5, LetrecFound5} = annotate_maybe_error(cerl:try_handler(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      NewIgnoreFound = IgnoreFound1 or IgnoreFound2 or IgnoreFound3 or IgnoreFound4 or IgnoreFound5,
+      NewLetrecFound = sets:union([LetrecFound1, LetrecFound2, LetrecFound3, LetrecFound4, LetrecFound5]),
+      NewMaybe_Error = get_maybe_error(Arg),
+      {cerl:update_c_try(update_ann(Tree, NewMaybe_Error), Arg, Vars, Body, Evars, Handler), C1 or C2 or C3 or C4 or C5, sets:union([Found1, Found2, Found3, Found4, Found5]), NewIgnoreFound, NewLetrecFound};
+    tuple ->
+      {Es, C, Found, IgnoreFound, LetrecFound} = annotate_maybe_error_all(cerl:tuple_es(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      NewMaybe_Error = get_all_maybe_error(Es),
+      {cerl:update_c_tuple(update_ann(Tree, NewMaybe_Error), Es), C, Found, IgnoreFound, LetrecFound};
+    values ->
+      {Es, C, Found, IgnoreFound, LetrecFound} = annotate_maybe_error_all(cerl:values_es(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+      NewMaybe_Error = get_all_maybe_error(Es),
+      {cerl:update_c_values(update_ann(Tree, NewMaybe_Error), Es), C, Found, IgnoreFound, LetrecFound};
+    var ->
+      %% If Force is true, we have to add the variable
+      %% To the Found return value, in order for parent lets
+      %% to know where their variables were used to.
+      Found =
+        case Force of
+          true -> sets:add_element(cerl:var_name(Tree), sets:new());
+          false -> sets:new()
+        end,
+      case dict:find(cerl:var_name(Tree), SM) of
+        {ok, {Value, _}} ->
+          {update_ann(Tree, Value), Value =/= CurMaybe_Error, Found, false, sets:new()};
+        error ->
+          {update_ann(Tree, true), true =/= CurMaybe_Error, Found, false, sets:new()}
+      end;
+    _ ->
+      {update_ann(Tree, true), true =/= CurMaybe_Error, sets:new(), false, sets:new()}
+  end.
+
+%% Handles apply nodes.
+annotate_maybe_error_apply(Tree, SM, Force, Ignored, LetrecIgnored, Mod, CurMaybe_Error) ->
+  Op = cerl:apply_op(Tree),
+  {Op1, C1, IgnoreFound1, LetrecFound1} =
+    case cerl:type(Op) of
+      var ->
+        %% We are applying a var.
+        case cerl:var_name(Op) of
+          {F, A} ->
+            %% It is of the form {F, A} so we search for the corresponding Mfa to the symbol table.
+            case dict:find({Mod, F, A}, SM) of
+              {ok, {Value, 'fun'}} ->
+                %% If it is in the symbol table we check its 'maybe_error' annotation.
+                case Value of
+                  type_dependent ->
+                    %% It is type_dependent so we have to check whether the application
+                    %% node has been typed succesfully. If it has, it is a safe application.
+                    case cuter_spec_checker:get_cerl_type(Tree) of
+                      notype -> {update_ann(Op, true), true =/= CurMaybe_Error, false, sets:new()};
+                      _ -> {update_ann(Op, type_dependent), type_dependent =/= CurMaybe_Error, false, sets:new()}
+                    end;
+                  _ -> {update_ann(Op, Value), Value =/= CurMaybe_Error, false, sets:new()}
+                end;
+              error ->
+                case dict:find({F, A}, SM) of
+                  {ok, {Value, FunType}} when FunType =:= 'fun' orelse FunType =:= letvar ->
+                    case Value of
+                      type_dependent ->
+                        case cuter_spec_checker:get_cerl_type(Tree) of
+                          notype -> {update_ann(Op, true), true =/= CurMaybe_Error, false, sets:new()};
+                          _ -> {update_ann(Op, type_dependent), type_dependent =/= CurMaybe_Error, false, sets:new()}
+                        end;
+                      _ -> 
+                        {update_ann(Op, Value), Value =/= CurMaybe_Error, false, sets:new()}
+                    end;
+                  error ->
+                    case sets:is_element({Mod, F, A}, Ignored) of
+                      false ->
+                        case sets:is_element({F, A}, LetrecIgnored) of
+                          true ->
+                            {Op, false, false, sets:from_list([{F, A}])};
+                          false ->
+                            {update_ann(Op, true), true =/= CurMaybe_Error, false, sets:new()}
+                        end;
+                      true ->
+                        {update_ann(Op, false), false =/= CurMaybe_Error, true, sets:new()}
+                    end
+                end
+            end;
+          Name ->
+            case dict:find(Name, SM) of
+              {ok, {Value, _FunType}} ->
+                case Value of
+                  type_dependent ->
+                    case cuter_spec_checker:get_cerl_type(Tree) of
+                      notype -> {update_ann(Op, true), true =/= CurMaybe_Error, false};
+                      _ -> {update_ann(Op, type_dependent), type_dependent =/= CurMaybe_Error, false, sets:new()}
+                    end;
+                  _ -> 
+                    {update_ann(Op, Value), Value =/= CurMaybe_Error, false, sets:new()}
+                end;
+              _ ->
+                {update_ann(Op, true), true =/= CurMaybe_Error, false, sets:new()}
+            end
+        end;
+      _ ->
+        error("unhandled op")
+    end,
+  {Args, C2, Found, IgnoreFound2, LetrecFound2} = annotate_maybe_error_all(cerl:apply_args(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+  NewMaybe_Error = maybe_error_or([get_maybe_error(Op1), get_all_maybe_error(Args)]),
+  case get_all_maybe_error(Args) of 
+    true ->
+      Tree1 = add_distrust_type_dependent(Tree);
+    _ -> 
+      Tree1 = Tree
+  end,
+  {cerl:update_c_apply(update_ann(Tree1, NewMaybe_Error), Op1, Args), C1 or C2, Found, IgnoreFound1 or IgnoreFound2, sets:union([LetrecFound1, LetrecFound2])}.
+
+%% Same as apply but we don't check for closures.
+annotate_maybe_error_call(Tree, SM, Force, Ignored, LetrecIgnored, Mod, CurMaybe_Error) ->
+  ModName = cerl:call_module(Tree),
+  Name = cerl:call_name(Tree),
+  Arity = length(cerl:call_args(Tree)),
+  {NewAnn, IgnoreFound1} = 
+    case cerl:is_literal(ModName) andalso cerl:is_literal(Name) of
+      true ->
+        case dict:find({element(3, ModName), element(3, Name), Arity}, SM) of
+          {ok, {Value, 'fun'}} ->
+            case Value of
+              type_dependent ->
+                case cuter_spec_checker:get_cerl_type(Tree) of
+                  notype -> {true,  false};
+                  _ -> {type_dependent, false}
+                end;
+              _ -> {Value, false}
+            end;
+          _ ->
+            case sets:is_element({element(3, ModName), element(3, Name), Arity}, Ignored) of
+              false ->
+                {true, false};
+              true ->
+                {true, true}
+            end
+        end;
+      _ -> throw("Unsupported call")
+    end,
+  {Args, C1, Found, IgnoreFound2, LetrecFound} = annotate_maybe_error_all(cerl:call_args(Tree), SM, Force, Ignored, LetrecIgnored, Mod),
+  NewMaybe_Error = maybe_error_or([NewAnn, get_all_maybe_error(Args)]),
+  C2 = NewMaybe_Error =/= CurMaybe_Error,
+  case get_all_maybe_error(Args) of
+    true ->
+      Tree1 = add_distrust_type_dependent(Tree);
+    _ -> 
+      Tree1 = Tree
+  end,
+  {cerl:update_c_call(update_ann(Tree1, NewMaybe_Error), ModName, Name, Args), C1 or C2, Found, IgnoreFound1 or IgnoreFound2, LetrecFound}.
+
+%% Letrec nodes do a fixpoint on their functiosn that they introduce.
+annotate_maybe_error_letrec(Tree, SM, Force, Ignored, LetrecIgnored, Mod, CurMaybe_Error) ->
+  {Names, Funsb} = lists:unzip(cerl:letrec_defs(Tree)),
+  FunNames = [cerl:var_name(Name) || Name <- Names],
+  FunNames1 = sets:from_list(FunNames),
+  NewIgnored = sets:union(LetrecIgnored, FunNames1),
+  {Funs, C1, Found1, IgnoreFound1, LetrecFound1} = annotate_maybe_error_letrec_fix(FunNames, Funsb, SM, Force, Ignored, NewIgnored, Mod, false),
+  SM1 = put_vars(Names, [{get_maybe_error_pessimistic(A), letvar} || A <- Funs], SM),
+  {Body, C2, Found2, IgnoreFound2, LetrecFound2} = annotate_maybe_error(cerl:letrec_body(Tree), SM1, Force, Ignored, LetrecIgnored, Mod),
+  NewMaybe_Error = get_maybe_error(Body),
+  Change = C1 or C2 or (CurMaybe_Error =/= NewMaybe_Error),
+  {cerl:update_c_letrec(update_ann(Tree, NewMaybe_Error), lists:zip(Names, Funs), Body), Change, sets:union([Found1, Found2]), IgnoreFound1 or IgnoreFound2, sets:union([LetrecFound1, LetrecFound2])}.
+
+%% The fix-point computation for letrec nodes.
+annotate_maybe_error_letrec_fix(Names, Funsb, SM, Force, Ignored, LetrecIgnored, Mod, Acc) ->
+  %% Annotate everything.
+  {Funs, C, Found, IgnoreFound, LetrecFound} = annotate_maybe_error_all(Funsb, SM, Force, Ignored, LetrecIgnored, Mod),
+  %% Filter Found applications belonging to this letrec node.
+  ThisLetrecFound = sets:filter(fun(X) -> cuter_graphs:list_contains(X, Names) end, LetrecFound),
+  %% If something changed or we found functions called from this SCC, run again.
+  case C or (sets:size(ThisLetrecFound) > 0) of
+    true ->
+      SM1 = put_vars_by_name(Names, [{get_maybe_error_pessimistic(A), letvar} || A <- Funs], SM),
+      annotate_maybe_error_letrec_fix(Names, Funs, SM1, Force, Ignored, LetrecIgnored, Mod, C or Acc);
+    false ->
+      RestLetrecFound = sets:filter(fun(X) -> not cuter_graphs:list_contains(X, Names) end, LetrecFound),
+      {Funs, Acc, Found, IgnoreFound, RestLetrecFound}
+  end.
+
+%% Annotates a pattern tree. This is considerably different since patterns
+%% have only specific nodes.
+annotate_maybe_error_pattern(Tree, SM, Force) ->
+  CurMaybe_Error = get_maybe_error(Tree),
+  case cerl:type(Tree) of
+    literal ->
+      {update_ann(Tree, false), true == CurMaybe_Error, sets:new(), SM};
+    var ->
+      Found =
+        case Force of
+          true -> sets:add_element(cerl:var_name(Tree), sets:new());
+          false -> sets:new()
+        end,
+      case dict:find(cerl:var_name(Tree), SM) of
+        {ok, {Value, _}} ->
+          {update_ann(Tree, Value), Value =/= CurMaybe_Error, Found, SM};
+        error ->
+          {update_ann(Tree, false), false =/= CurMaybe_Error, Found, put_vars([Tree], [{type_dependent, 'var'}], SM)}
+      end;
+    cons ->
+      {Hd, C1, Found1, SM1} = annotate_maybe_error_pattern(cerl:cons_hd(Tree), SM, Force),
+      {Tl, C2, Found2, SM2} = annotate_maybe_error_pattern(cerl:cons_tl(Tree), SM1, Force),
+      NewMaybe_Error = maybe_error_or([get_maybe_error(Hd), get_maybe_error(Tl)]),
+      {cerl:update_c_cons_skel(update_ann(Tree, NewMaybe_Error), Hd, Tl), C1 or C2, sets:union([Found1, Found2]), SM2};
+    tuple ->
+      {Es, C, Found, SM1} = annotate_maybe_error_pattern_all(cerl:tuple_es(Tree), SM, Force),
+      NewMaybe_Error = get_all_maybe_error(Es),
+      {cerl:update_c_tuple(update_ann(Tree, NewMaybe_Error), Es), C, Found, SM1};
+    alias ->
+      {Pat, C1, Found, SM1} = annotate_maybe_error_pattern(cerl:alias_pat(Tree), SM, Force),
+      Var = cerl:alias_var(Tree),
+      SM2 = put_vars([Var], [{type_dependent, 'var'}], SM1),
+      Var1 = update_ann(Var, type_dependent),
+      Tree1 = update_ann(Tree, type_dependent),
+      C2 = CurMaybe_Error =/= type_dependent,
+      {cerl:update_c_alias(Tree1, Var1, Pat), C1 or C2, Found, SM2}
+  end.
+
+get_arg_maybe_errors(Arg) ->
+  [{get_maybe_error_pessimistic(Arg), letvar}].
+
+%% Wrapper for annotate_maybe_error/6 for a list of nodes.
+annotate_maybe_error_all(Trees, SM, Force, Ignored, LetrecIgnored, Mod) ->
+  X = [annotate_maybe_error(T, SM, Force, Ignored, LetrecIgnored, Mod) || T <- Trees],
+  Or = fun(E) -> fun(A, B) -> B or element(E, A) end end,
+  {[element(1, Y) || Y <- X], lists:foldl(Or(2), false, X), sets:union([element(3, Z) || Z <- X]), lists:foldl(Or(4), false, X), sets:union([element(5, Z) || Z <- X])}.
+
+%% Wrapper for annotate_maybe_error_pattern/3 for a list of patterns.
+annotate_maybe_error_pattern_all(Trees, SM, Force) ->
+  annotate_maybe_error_pattern_all(Trees, SM, Force, [], false, sets:new()).
+
+annotate_maybe_error_pattern_all([], SM, _, AccTrees, AccC, AccFound) -> {lists:reverse(AccTrees), AccC, AccFound, SM};
+annotate_maybe_error_pattern_all([Tree|Trees], SM, Force, AccTrees, AccC, AccFound) ->
+  {NewTree, C, Found, SM1} = annotate_maybe_error_pattern(Tree, SM, Force),
+  annotate_maybe_error_pattern_all(Trees, SM1, Force, [NewTree|AccTrees], C or AccC, sets:union([AccFound, Found])).
+
+%% Fetches the maybe_error annotation of a cerl node.
+get_maybe_error(Tree) ->
+  Anno = cerl:get_ann(Tree),
+  get_maybe_error_anno(Anno).
+
+%% Fetches the maybe_error annotation in a list of annotations.
+get_maybe_error_anno([]) -> false;
+get_maybe_error_anno([{maybe_error, V}|_]) -> V;
+get_maybe_error_anno([_|Tl]) -> get_maybe_error_anno(Tl).
+
+%% Fetches the 'maybe_error_annotation' of a node as true false
+%% depending on the value of DT.
+%% DT == true ==> type_dependent == true
+%% DT == false ==> type_dependent == false
+-spec get_maybe_error_bin(cerl:cerl(), boolean()) -> boolean().
+get_maybe_error_bin(Tree, DT) ->
+  Anno = cerl:get_ann(Tree),
+  get_maybe_error_bin_anno(Anno, DT).
+
+%% Fetches the 'maybe_error_annotation' like get_maybe_error_bin/2 but
+%% given the list of annotations directly.
+-spec get_maybe_error_bin_anno([any()], boolean()) -> boolean().
+get_maybe_error_bin_anno([], _DT) -> true;
+get_maybe_error_bin_anno([{maybe_error, V}|_], DT) -> 
+  case V of
+    type_dependent -> DT;
+    V1 -> V1
+  end;
+get_maybe_error_bin_anno([_|Tl], DT) -> get_maybe_error_bin_anno(Tl, DT).
+
+%% Fetches the maybe_error annotation considering non
+%% annotated notes as having a true annotation
+get_maybe_error_pessimistic(Tree) ->
+  get_maybe_error_pessimistic_anno(cerl:get_ann(Tree)).
+
+get_maybe_error_pessimistic_anno([]) -> true;
+get_maybe_error_pessimistic_anno([{maybe_error, V}|_]) -> V; 
+get_maybe_error_pessimistic_anno([_|Tl]) -> get_maybe_error_pessimistic_anno(Tl).
+
+%% Returns a list of 'maybe_error' annotations given a list of nodes.
+get_all_maybe_error(Trees) ->
+  maybe_error_or([get_maybe_error(T) || T <- Trees, not cuter_spec_checker:get_type_dependent_unreachable(T)]).
+
+%% Returns true if at least one variable in a list given
+%% as the first argument is part of a set given as the second argument.
+vars_in_set([], _) -> false;
+vars_in_set([Hd|Tl], Set) ->
+  case sets:is_element(cerl:var_name(Hd), Set) of
+    true ->
+      true;
+    false ->
+      vars_in_set(Tl, Set)
+  end.
+
+%% Fetches the 'force_constraint_logging' annotation.
+-spec get_force_constraint_logging([any()]) -> boolean().
+get_force_constraint_logging([]) -> false;
+get_force_constraint_logging([Hd|Tl]) ->
+  case Hd of
+    {force_constraint_logging, Value} ->
+      Value;
+    _ ->
+      get_force_constraint_logging(Tl)
+  end.
+
+%% Fetches the 'distrust_type_dependent' annotation.
+-spec get_distrust_type_dependent([any()]) -> boolean().
+get_distrust_type_dependent([]) -> false;
+get_distrust_type_dependent([Hd|Tl]) ->
+  case Hd of
+    {distrust_type_dependent, Value} ->
+      Value;
+    _ ->
+      get_distrust_type_dependent(Tl)
+  end.
+
+%% Binary operator between two 'maybe_error' annotations.
+maybe_error_or(E) ->
+  lists:foldl(
+    fun(A, B) ->
+        case A of
+          true -> true;
+          false -> B;
+          type_dependent ->
+            case B of
+              true -> true;
+              _ -> type_dependent
+            end
+        end
+    end,
+    false,
+    E
+   ).
+
+%% Returns whether there is an unreachable clause in a set of clauses.
+unreachable_clauses(Clauses) ->
+  lists:foldl(fun(Clause, Acc) -> Acc orelse cuter_spec_checker:get_type_dependent_unreachable(Clause) end, false, Clauses).
+
+%% Creates the flags needed to input to put_vars/3.
+make_fun_flags(Vars) ->
+  Fn = fun(Var) ->
+           case cuter_spec_checker:get_cerl_type(Var) of
+             notype -> {false, var};
+             T ->
+               case erl_types:t_is_fun(T) of
+                 true -> {type_dependent, var};
+                 false -> {false, var}
+               end
+           end
+       end,
+  lists:map(Fn, Vars).
+
+%% ================================================================================
+%% The preprocess function:
+%% Takes an entry point {M, F, A}, calculates the callgraph with this entrypoint as
+%% its root, merges the nodes belonging to a cycle until the callgraph is a DAG and
+%% then annotates it from the leaves to the root, in a DFS order
+%% ================================================================================
+
+-spec preprocess(mfa(), dict:dict(), dict:dict()) -> dict:dict().
+preprocess(EntryPoint, KFunctionASTS, MfasToSpecs) ->
+  FunctionASTS = 
+    dict:map(
+      fun(_, Value) ->
+          cuter_cerl:kfun_code(Value)
+      end,
+      KFunctionASTS
+     ),
+  {CallGraph, Funs, NewEntryPoint} = cuter_graphs:calculate_dag_callgraph(EntryPoint),
+  TypedASTS = cuter_spec_checker:annotate_types(FunctionASTS, MfasToSpecs, Funs),
+  AnnotatedASTS = annotate_callgraph(NewEntryPoint, TypedASTS, CallGraph),
+  dict:map(
+    fun(Key, Value) ->
+        cuter_cerl:kfun_update_code(Value, dict:fetch(Key, AnnotatedASTS))
+    end,
+    KFunctionASTS
+   ).
diff --git a/src/cuter_spec_checker.erl b/src/cuter_spec_checker.erl
new file mode 100644
index 00000000..8b1abf0d
--- /dev/null
+++ b/src/cuter_spec_checker.erl
@@ -0,0 +1,1161 @@
+-module(cuter_spec_checker).
+-export([get_cerl_type/1, get_type_dependent_unreachable/1, annotate_types/3]).
+
+%% ==========
+%% Used types
+%% ==========
+
+-type function_ast_dict() :: dict:dict(mfa(), cerl:cerl()).
+-type function_sig_dict() :: dict:dict(mfa(), [erl_types:erl_type()]).
+-type function_set() :: sets:set(mfa()).
+
+%% =========================
+%% Multi function annotation
+%% =========================
+
+%% Entry point for the type annotation of the function ASTs.
+%% Arguments:
+%% FunctionASTS: dictionary with Mfas as keys and ASTs as values.
+%% Sigs: dictionary with Mfas as keys and lists of erl_types as values.
+%% FSet: Set of all functions in the callgraph.
+%% Returns:
+%% The annotated function ASTs in a dictionary with their Mfas as keys.
+-spec annotate_types(function_ast_dict(), function_sig_dict(), function_set()) -> function_ast_dict().
+annotate_types(FunctionASTS, Sigs, FSet) ->
+  %% Initialize the symbol table using the original_tsm defined in cuter_type_dependent_functions
+  %% adding the signatures of the functions we want to annotate too.
+  TSM = 
+    lists:foldl(
+      fun ({MFA, Sig}, T) ->
+          dict:store(MFA, Sig, T)
+      end,
+      cuter_type_dependent_functions:original_tsm(),
+      dict:to_list(Sigs)
+     ),
+  %% NoSpec will hold the funtions with no signatures.
+  %% We need to know which of them do not originally have signatures
+  %% to allow altering their signature when we find calls to them.
+  NoSpec = find_nospec(FSet, Sigs),
+  %% OpenSet will hold the Mfas of functions we want to traverse.
+  %% It also contains a persistence dictionary for each function to avoid
+  %% infinite loops in recursive letrec.
+  OpenSet = make_open_set(FSet, Sigs),
+  annotate_types_helper(FunctionASTS, TSM, OpenSet, NoSpec).
+
+%% Performs the fix point computation over the functions in OpenSet.
+%% While OpenSet has elements, the annotation algorithm is ran upon the
+%% whole OpenSet.
+annotate_types_helper(FunctionASTS, TSM, OpenSet, NoSpec) ->
+  case length(OpenSet) of
+    0 -> FunctionASTS;
+    _ ->
+      {FASTS1, TSM1, OpenSet1} = annotate_types_helper_pass(FunctionASTS, TSM, OpenSet, NoSpec),
+      annotate_types_helper(FASTS1, TSM1, OpenSet1, NoSpec)
+  end.
+
+%% Calls the annotation on each function in the OpenSet.
+annotate_types_helper_pass(FunctionASTS, TSM, OpenSet, NoSpec) ->
+  %% Do it with a tail recursive function.
+  annotate_types_helper_pass(FunctionASTS, TSM, OpenSet, NoSpec, []).
+
+annotate_types_helper_pass(FunctionASTS, TSM, [], _NoSpec, OpenSet1) -> {FunctionASTS, TSM, lists:reverse(OpenSet1)};
+annotate_types_helper_pass(FunctionASTS, TSM, [{Mfa, Persistence}|Mfas], NoSpec, OpenSet1) ->
+  %% Fetch the function AST.
+  AST = dict:fetch(Mfa, FunctionASTS),
+  %% Fetch the function Spec.
+  Spec = dict:fetch(Mfa, TSM),
+  %% Add the persistene to the symbol table
+  TSMP = merge_all_dicts([TSM, Persistence]),
+  %% Run the annotation on the AST.
+  {NewAST, D, C, P} = pass_down_fun_types(Mfa, AST, Spec, TSMP, NoSpec),
+  %% Update the symbol table and the open set.
+  {TSM1, OpenSet2} = update_from_detected(D, TSM, OpenSet1),
+  %% If there has been some change in the annotations of the funtion or
+  %% calls to functions that do not much the current signature have been detected:
+  case C or (length(D) > 0) of
+    true -> %% Add the functions that should be traversed again in OpenSet.
+      OpenSet3 = update_open_set(Mfa, P, OpenSet2);
+    false -> %% Else do not update the OpenSet.
+      OpenSet3 = OpenSet2
+  end,
+  %% Check if the current function is part of the NoSpec set.
+  case sets:is_element(Mfa, NoSpec) of
+    true -> %% If it is then
+      %% fetch its type from its AST.
+      T = get_cerl_type(NewAST),
+      %% Check if it has been typed succesfully.
+      case erl_types:is_erl_type(T) of
+        true -> %% If it has then
+          %% update its signature in the symbol table.
+          [S] = dict:fetch(Mfa, TSM1),
+          NewS = erl_types:t_fun(erl_types:t_fun_args(S), T),
+          TSM2 = dict:store(Mfa, [NewS], TSM1);
+        false -> TSM2 = TSM1
+      end;
+    false ->
+      TSM2 = TSM1
+  end,
+  %% Update its AST in the dictionary.
+  NewASTS = dict:store(Mfa, NewAST, FunctionASTS),
+  annotate_types_helper_pass(NewASTS, TSM2, Mfas, NoSpec, OpenSet3).
+
+%% Updates the open set for a specific Mfa.
+%% If this Mfa is already in the open set,
+%% puts it in the end of the open set, else
+%% just append it.
+update_open_set(Mfa, P, OpenSet) ->
+  lists:reverse([{Mfa, P}|update_open_set1(Mfa, OpenSet, [])]).
+
+update_open_set1(_Mfa, [], Acc) -> Acc;
+update_open_set1(Mfa, [{Mfa, _P}|Rest], Acc) ->
+  update_open_set1(Mfa, Rest, Acc);
+update_open_set1(Mfa, [A|R], Acc) ->
+  update_open_set1(Mfa, R, [A|Acc]).
+
+%% Updates the open set and symbol table
+%% from detected function calls
+%% to functions that are in the NoSpec set.
+update_from_detected([], TSM, OpenSet) -> {TSM, OpenSet};
+update_from_detected([{Mfa, Spec}|Rest], TSM, OpenSet) ->
+  OpenSet1 = [{Mfa, dict:new()}|OpenSet],
+  case dict:find(Mfa, TSM) of
+    {ok, [Cur]} ->
+      TSM1 = dict:store(Mfa, [erl_types:t_sup(Cur, Spec)], TSM);
+    error ->
+      TSM1 = dict:store(Mfa, [Spec], TSM)
+  end,
+  update_from_detected(Rest, TSM1, OpenSet1).
+
+%% Finds which functions don't have a signature from the Fset.
+find_nospec(FSet, Sigs) ->
+  Fn = fun(F) -> not dict:is_key(F, Sigs) end,
+  sets:filter(Fn, FSet).
+
+%% Creates the initial open set.
+%% The open set is just a queue containing tuples of the form:
+%% {Mfa, Persistence}
+make_open_set(FSet, Sigs) ->
+  Fn = fun(F) ->
+           case dict:is_key(F, Sigs) of
+             true -> length(dict:fetch(F, Sigs)) =:= 1;
+             false -> false
+           end
+       end,
+  O1 = sets:to_list(sets:filter(Fn, FSet)),
+  [{X, dict:new()} || X <- O1].
+
+%% ==========================
+%% Single function annotation
+%% ==========================
+
+%% Returns the type type of a node given its list of annotations.
+%% The type could be an erl_type or 'notype'.
+get_type([]) -> notype;
+get_type([Hd|Tl]) ->
+  case Hd of
+    {node_type, Value} ->
+      Value;
+    _ ->
+      get_type(Tl)
+  end.
+
+%% Same as get_type but it is given the actual cerl node.
+-spec get_cerl_type(cerl:cerl()) -> erl_types:erl_type() | notype.
+get_cerl_type(T) -> get_type(cerl:get_ann(T)).
+
+%% Updates the type of a cerl node to the given one altering its annotation list.
+update_type(Tree, Type) ->
+  Anno = cerl:get_ann(Tree),
+  cerl:set_ann(Tree, update_type(Anno, Type, [], false)).
+
+update_type([], Type, Acc, false) -> [{node_type, Type}|Acc];
+update_type([], _, Acc, true) -> Acc;
+update_type([{node_type, _}|T], Type, Acc, _) -> update_type(T, Type, [{node_type, Type}|Acc], true);
+update_type([H|T], Type, Acc, Found) -> update_type(T, Type, [H|Acc], Found).
+
+%% Adds the annotation 'type_dependent_unreachable' to the list of annotations
+%% of the given cerl node representing a case clause.
+mark_as_unreachable(Clause) ->
+  Anno = cerl:get_ann(Clause),
+  case cuter_graphs:list_contains(type_dependent_unreachable, Anno) of
+    false ->
+      cerl:add_ann([type_dependent_unreachable], Clause);
+    true ->
+      Clause
+  end.
+
+%% Removes the 'type_dependent_unreachable' annotation from the list of annotations
+%% of a case clause.
+mark_as_reachable(Clause) ->
+  Anno = [T || T <- cerl:get_ann(Clause), T =/= type_dependent_unreachable],
+  cerl:set_ann(Clause, Anno).
+
+%% Returns whether the tree node has a type in its annotations.
+%% If the tree node has the type 'notype' then it is considered as not having a type.
+has_type(Tree) ->
+  Anno = cerl:get_ann(Tree),
+  lists:foldl(
+    fun erlang:'or'/2,
+    false,
+    lists:map(
+      fun(A) ->
+          case A of
+            {node_type, T} when T =/= notype -> true;
+            _ -> false
+          end
+      end,
+      Anno
+     )
+   ).
+
+%% Returns a list of types given a list of cerl nodes.
+arg_types(Args) ->
+  lists:map(fun get_cerl_type/1, Args).
+
+%% Returns a list of argument types of a 'let' node.
+%% If the 'let' node is just on one term, it returns a list containint
+%% just the type of this term. If it is a 'values' node, it returns a list
+%% containing all of the types inside the 'values' node.
+let_arg_types(Arg) ->
+  case cerl:type(Arg) of
+    values ->
+      arg_types(cerl:values_es(Arg));
+    _ -> [get_cerl_type(Arg)]
+  end.
+
+%% Introduces variables Vars in the symbol table TSM with types Types.
+put_vars(Vars, Types, TSM) ->
+  F =
+    fun({Var, Type}, B) ->
+        case Type of
+          notype -> B;
+          [notype] -> B;
+          _ -> dict:store(cerl:var_name(Var), Type, B)
+        end
+    end,
+  lists:foldl(F, TSM, lists:zip(Vars, Types)).
+
+%% =====================
+%% Helper type functions
+%% =====================
+
+%% Takes a cerl node representing a pattern in a case clause and
+%% creates an equivalent erl_type. It takes TSM2 as an argument,
+%% which holds all the variables contained in the guard of the specific
+%% clause. If these variables are encountered, they get replaced by the
+%% erl_type they are forced to have by the guard. If any other variables
+%% are encountered, they are either replaced with erl_types:t_any() if they
+%% are not in the symbol table or erl_types:t_none() if they exist in the
+%% symbol table.
+t_from_pattern(Tree, TSM, TSM2) ->
+  case cerl:type(Tree) of
+    literal ->
+      erl_types:t_from_term(element(3, Tree));
+    var ->
+      case dict:find(cerl:var_name(Tree), TSM2) of
+        {ok, Type} ->
+          Type;
+        error ->
+          case dict:find(cerl:var_name(Tree), TSM) of
+            {ok, _} -> erl_types:t_none();
+            error ->
+              erl_types:t_any()
+          end
+      end;
+    cons ->
+      Hd = t_from_pattern(cerl:cons_hd(Tree), TSM, TSM2),
+      Tl = t_from_pattern(cerl:cons_tl(Tree), TSM, TSM2),
+      case erl_types:t_is_nil(Tl) of
+        true -> erl_types:t_none();
+        false ->
+          case erl_types:t_is_none(Tl) of
+            true -> erl_types:t_none();
+            false -> erl_types:t_cons(Hd, Tl)
+          end
+      end;
+    tuple ->
+      Es = lists:map(fun(E) -> t_from_pattern(E, TSM, TSM2) end, cerl:tuple_es(Tree)),
+      erl_types:t_tuple(Es);
+    alias ->
+      Pat = cerl:alias_pat(Tree),
+      t_from_pattern(Pat, TSM, TSM2);
+    _ -> erl_types:t_none()
+  end.
+
+%% Returns the type of the result of a function call
+%% given the types of its arguments.
+application_type(Spec, ArgTypes) when not is_list(Spec) ->
+  application_type([Spec], ArgTypes);
+application_type([], _) -> error;  
+application_type([Spec|Specs], ArgTypes) ->
+  SpecArgs = erl_types:t_fun_args(Spec),
+  case lists:foldl(
+         fun erlang:'and'/2,
+         true,
+         lists:zipwith(
+           fun erl_types:t_is_subtype/2,
+           lists:map(
+             fun(A) ->
+                 case A of
+                   notype -> erl_types:t_any();
+                   B -> B
+                 end
+             end,
+             ArgTypes),
+           SpecArgs)) of
+    true ->
+      {ok, erl_types:t_fun_range(Spec)};
+    false ->
+      application_type(Specs, ArgTypes)
+  end.
+
+%% Just a wrapper of erl_types:t_sup/1 to create a union.
+t_union(Types) ->
+  erl_types:t_sup(Types).
+
+%% The term unify is not exact in this case.
+%% This function takes a cerl node of a clause pattern
+%% and an erl_type. Its purpose is to find the values of
+%% all variables in the cerl tree, such that if this cerl
+%% tree was an erl_type, it would be a valid subtype of
+%% Type. Again, TSM is the symbol table and TSM2 holds all the
+%% variables encountered in the guard of the clause with their
+%% constrained types.
+unify_pattern(Tree, TSM, TSM2, Type) ->
+  %% We distinguish cases depending on the type of the cerl node Tree.
+  case cerl:type(Tree) of
+    literal ->
+      %% If it is a literal, then we have no variables left to assign types.
+      {ok, TSM};
+    var ->
+      %% If it is a var, we check whether it is in the symbol table.
+      case dict:find(cerl:var_name(Tree), TSM) of
+        {ok, VarType} ->
+          %% If it is, then we check whether its type can be unified
+          %% with Type.
+          try erl_types:t_unify(VarType, Type) of
+            _ -> {ok, TSM}
+          catch
+            _ -> {error, mismatch}
+          end;
+        error ->
+          %% If it is not, then we check if it is a part of TSM2.
+          case dict:find(cerl:var_name(Tree), TSM2) of
+            {ok, VarGuardType} ->
+              %% If it is, then if it is a supertype of Type, we store it in the symbol table
+              case erl_types:t_is_subtype(Type, VarGuardType) of
+                true -> {ok, dict:store(cerl:var_name(Tree), VarGuardType, TSM)};
+                false -> {error, mismatch}
+              end;
+            error ->
+              %% If it is a new variable, it has to have the type Type.
+              {ok, dict:store(cerl:var_name(Tree), Type, TSM)}
+          end
+      end;
+    cons ->
+      %% If it is a cons, we check if Type is a list.
+      case erl_types:t_is_list(Type) of
+        true ->
+          %% If it is, we recursively do the same for its values.
+          NewType = erl_types:t_nonempty_list(erl_types:t_list_elements(Type)),
+          Hdt = unify_pattern(cerl:cons_hd(Tree), TSM, TSM2, erl_types:t_cons_hd(NewType)),
+          case Hdt of
+            {ok, TSM1} ->
+              Tlt = unify_pattern(cerl:cons_tl(Tree), TSM1, TSM2, erl_types:t_cons_tl(NewType)),
+              case Tlt of
+                {ok, TSMnew} -> {ok, TSMnew};
+                _ -> {error, mismatch}
+              end;
+            _  ->
+              {error, mismatch}
+          end;
+        false ->
+          %% If Type is not a list, it might be a union of a list and something else.
+          %% In this case, we want to do this procedure for the list part of the union,
+          %% which is done with the function below.
+          try_to_handle_union(Tree, TSM, TSM2, Type, erl_types:t_list())
+      end;
+    tuple ->
+      %% Tuple is similar to list. We check if Type is also a tuple.
+      case erl_types:t_is_tuple(Type) of
+        true ->
+          %% If it is, we recursively do this procedure for its values.
+          Type1 = 
+            try erl_types:t_tuple_size(Type) of
+              _ -> Type
+            catch
+              _:_ -> erl_types:t_tuple(length(cerl:tuple_es(Tree)))
+            end,
+          case length(cerl:tuple_es(Tree)) == erl_types:t_tuple_size(Type1) of
+            true -> 
+              lists:foldl(
+                fun({E, Et}, V) ->
+                    case V of
+                      {ok, V1} ->
+                        unify_pattern(E, V1, TSM2, Et);
+                      {error, _} ->
+                        {error, mismatch}
+                    end
+                end,
+                {ok, TSM},
+                lists:zip(cerl:tuple_es(Tree), erl_types:t_tuple_args(Type1))
+               );
+            false -> {error, mismatch}
+          end;
+        false ->
+          %% If it is not, it might be a union of a tuple and something else.
+          %% Again, we would want to do this procedure for the tuple part of the list.
+          try_to_handle_union(Tree, TSM, TSM2, Type, erl_types:t_tuple())
+      end;
+    _ ->
+      %% TODO: maps, bistrings. For now we just return TSM as is. If we don't
+      %% add the variables in the symbol table, they won't be constrained, so
+      %% we will overaproximate any subsequent types. This might result in
+      %% some nodes being annotated with 'maybe_error' equal to true, which
+      %% is pessimistic and leaves our analysis sound.
+      {ok, TSM}
+  end.
+
+%% Checks whether Type is a union. If it is, then it tries
+%% to call unify_pattern/4 with the part of the union we
+%% are interested in.
+try_to_handle_union(Tree, TSM, TSM2, Type, T) ->
+  case erl_types:is_erl_type(Type) andalso erl_types:is_erl_type(T) of
+    true ->
+      H = erl_types:t_subtract(Type, (erl_types:t_subtract(Type, T))),
+      case erl_types:t_is_none(H) of
+        true -> {error, mismatch};
+        false -> unify_pattern(Tree, TSM, TSM2, H)
+      end;
+    false ->
+      {error, mismatch}
+  end.
+
+%% ==================
+%% Passing down types
+%% ==================
+
+%% This is the entry point for annotating the AST
+%% of a function with type information in each node.
+pass_down_fun_types({M, _F, _A}, AST, Spec, TSM, NoSpec) ->
+  pass_down_types_helper(AST, Spec, TSM, M, NoSpec).
+
+pass_down_types_helper(Fun, Spec, TSM, Mod, NoSpec) ->
+  TSM2 = put_vars(cerl:fun_vars(Fun), erl_types:t_fun_args(hd(Spec)), TSM),
+  {Body, D, C, _DC, P} = pass_down_types(cerl:fun_body(Fun), TSM2, Mod, notype, NoSpec, sets:new()),
+  {cerl:update_c_fun(Fun, cerl:fun_vars(Fun), Body), D, C, P}.
+
+%% Core of the analysis.
+%% Arguments:
+%% - Tree: The AST node under consideration.
+%% - TSM: Symbol table. It is a dictionary containint types of functiosn and variables.
+%% - Mod: The module in which the function is defined.
+%% - ArgType: Holds the type of the argument of the case construct this node is enclosed in (if there is one).
+%% - NoSpec: The set containing all the functions that originally had no specification.
+%% - Closures: A symbol table-like dictionary for closures defined in the function we are annotating.
+%% Returns:
+%% 1. The same tree node annotated with type information.
+%% 2. A list of tuples of the form {Mfa, erl_type} corresponding to calls to functions encountered 
+%%    belonging to NoSpec with their newly calculated types.
+%% 3. A boolean value representing whether annotations have changed in the current node or its children.
+%%    This is used for the fix-point computation.
+%% 4. Similar to 2 but for closures because let_rec nodes do their own fix-point computation.
+%% 5. Persistence table. It contains all the variables encountered inside closures so they are appended
+%%    to the symbol table if a function is annotated again. This way no infinite loops happen.
+%% Most node types don't perform any serious calculation. They just call this function recursively
+%% on their children and use combine the results to assign a type on themselves and return the
+%% desired values. Some nodes need more logic so they have their own functions.
+pass_down_types(Tree, TSM, Mod, ArgType, NoSpec, Closures) ->
+  CurType = get_cerl_type(Tree),
+  case cerl:type(Tree) of
+    alias ->
+      {Pat, D1, C1, CD1, P1} = pass_down_types(cerl:alias_pat(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      Var = cerl:alias_var(Tree),
+      T = get_cerl_type(Pat),
+      Var1 = update_type(Var, T),
+      Change = C1 or (CurType =/= T),
+      Tree1 = update_type(Tree, T),
+      {cerl:update_c_alias(Tree1, Var1, Pat), D1, Change, CD1, P1};
+    'apply' ->
+      pass_down_types_apply(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType);
+    call ->
+      pass_down_types_call(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType);
+    'case' ->
+      pass_down_types_case(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType);
+    clause ->
+      pass_down_types_clause(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType);
+    cons ->
+      {Hd, D1, C1, CD1, P1} = pass_down_types(cerl:cons_hd(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      {Tl, D2, C2, CD2, P2} = pass_down_types(cerl:cons_tl(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      %% Annotate types for head and tail. If at least one of them does not have a type, then
+      %% the whole list does not have a type either.
+      Tree1 = 
+        case {get_cerl_type(Hd), get_cerl_type(Tl)} of
+          {X, Y} when X =:= notype orelse Y =:= notype -> update_type(Tree, notype);
+          _ -> update_type(Tree, erl_types:t_cons(get_cerl_type(Hd), get_cerl_type(Tl)))
+        end,
+      Change = C1 or C2 or (CurType =/= get_cerl_type(Tree1)),
+      P = merge_all_dicts([P1, P2]),
+      {cerl:update_c_cons(Tree1, Hd, Tl), D1 ++ D2, Change, CD1 ++ CD2, P};
+    tuple ->
+      %% Annotate types for all members of the tuple. If at least one does not have a type,
+      %% mark the tuple as having no type as well.
+      {Es, D, C, CD, P} = pass_down_types_all(cerl:tuple_es(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      Tree1 =
+        case lists:foldl(fun(X, Y) -> Y orelse (get_cerl_type(X) =:= notype) end, false, Es) of
+          true ->
+            update_type(Tree, notype);
+          false -> update_type(Tree, erl_types:t_tuple(lists:map(fun get_cerl_type/1, Es)))
+        end,
+      Change = C or (CurType =/= get_cerl_type(Tree1)),
+      {cerl:update_c_tuple(Tree1, Es), D, Change, CD, P};
+    'fun' ->
+      pass_down_types_fun(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType);
+    'let' ->
+      pass_down_types_let(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType);
+    letrec ->
+      pass_down_types_letrec(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType);
+    literal ->
+      {update_type(Tree, erl_types:t_from_term(element(3, Tree))), [], false, [], dict:new()};
+    seq ->
+      %% The type of a seq node is the type of its body.
+      {Arg, D1, C1, CD1, P1} = pass_down_types(cerl:seq_arg(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      {Body, D2, C2, CD2, P2} = pass_down_types(cerl:seq_body(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      Change = C1 or C2 or (CurType =/= get_cerl_type(Body)),
+      P = merge_all_dicts([P1, P2]),
+      {cerl:update_c_seq(update_type(Tree, get_cerl_type(Body)), Arg, Body), D1 ++ D2, Change, CD1 ++ CD2, P};
+    'try' ->
+      {Arg, D1, C1, CD1, P1} = pass_down_types(cerl:try_arg(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      {Vars, D2, C2, CD2, P2} = pass_down_types_all(cerl:try_vars(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      {Body, D3, C3, CD3, P3} = pass_down_types(cerl:try_body(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      {Evars, D4, C4, CD4, P4} = pass_down_types_all(cerl:try_evars(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      {Handler, D5, C5, CD5, P5} = pass_down_types(cerl:try_handler(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      Change = C1 or C2 or C3 or C4 or C5 or (CurType =/= get_cerl_type(Body)),
+      D = lists:append([D1, D2, D3, D4, D5]),
+      CD = lists:append([CD1, CD2, CD3, CD4, CD5]),
+      P = merge_all_dicts([P1, P2, P3, P4, P5]),
+      {cerl:update_c_try(update_type(Tree, get_cerl_type(Body)), Arg, Vars, Body, Evars, Handler), D, Change, CD, P};
+    primop ->
+      %% We do not assign a type to a primop because it is considered to produce
+      %% errors by the subsequent analysis.
+      {update_type(Tree, notype), [], false, [], dict:new()};
+    values ->
+      %% The type of a values node is a tuple type with elements the types of the children of the values node.
+      %% This holds if all of them have a valid type.
+      {Es, D1, C1, CD1, P1} = pass_down_types_all(cerl:values_es(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+      case lists:all(fun has_type/1, Es) of
+        true ->
+          {cerl:update_c_values(update_type(Tree, erl_types:t_tuple([get_cerl_type(T) || T <- Es])), Es), D1, C1, CD1, P1};
+        false ->
+          {cerl:update_c_values(update_type(Tree, notype), Es), D1, C1 or (CurType =/= notype), CD1, P1}
+      end;
+    var ->
+      %% The type of a variable is the type it has been found to have in the symbol table.
+      %% If it is not in the symbol table then it has no type.
+      case dict:find(cerl:var_name(Tree), TSM) of
+        {ok, Type} ->
+          {update_type(Tree, Type), [], false, [], dict:new()};
+        _ -> {update_type(Tree, notype), [], false, [], dict:new()}
+      end;
+    _ ->
+      %% Catches rest not supported nodes. It annotates them with no type. This
+      %% might make nodes that are safe seem unsafe by the subsequent analysis
+      %% but not the other way around so we are sound.
+      {Tree, [], false, [], dict:new()}
+  end.
+
+%% Logic for when the tree is an apply node.
+%% Arguments and rerurn values are the same as pass_down_types/6
+%% with the current type additionally passed as an argument.
+pass_down_types_apply(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType) ->
+  %% Annotate types for arguments of the apply.
+  {Args, D1, C1, CD1, P1} = pass_down_types_all(cerl:apply_args(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+  %% Fetch the apply operation.
+  Op = cerl:apply_op(Tree),
+  {Tree1, D2, C2, CD2} =
+    %% Check if all arguments have types.
+    case lists:all(fun has_type/1, Args) of
+      true ->
+        %% If they do then distinguish between the possible forms of Op.
+        case cerl:type(Op) of
+          var ->
+            %% If Op is a variable, create the Mfa using the module we are currently in.
+            OpN = case cerl:var_name(Op) of {F, A} -> {Mod, F, A}; Name -> Name end,
+            %% Search for the function in the symbol table.
+            case dict:find(OpN, TSM) of
+              {ok, Specs} ->
+                %% If it is in the symbol table, fetch the type of the application.
+                case application_type(Specs, arg_types(Args)) of
+                  {ok, Type} ->
+                    %% If it is a valid type, we use this as the type of the apply node.
+                    {update_type(Tree, Type), D1, false, CD1};
+                  error ->
+                    %% Else the function may be in the NoSpec set and we have to update its signature
+                    %% to satisfy this call.
+                    case sets:is_element(OpN, NoSpec) of
+                      true ->
+                        %% If it is find its new type.
+                        NewSpec = rewrite_spec(arg_types(Args), Specs),
+                        {Tree, [{OpN, NewSpec} | D1], true, CD1};
+                      false ->
+                        %% If it is not, it might be a closure.
+                        case sets:is_element(OpN, Closures) of
+                          true ->
+                            %% If it is, update its spec.
+                            NewSpec = rewrite_spec(arg_types(Args), Specs),
+                            {Tree, D1, true, [{OpN, NewSpec} | CD1]};
+                          false ->
+                            %% If it is not, don't update the tree node.
+                            {Tree, D1, false, CD1}
+                        end
+                    end
+                end;
+              error ->
+                %% If it is not in the symbol table, then it might not have a spec.
+                case sets:is_element(OpN, NoSpec) of
+                  true ->
+                    %% If it is in the NoSpec set then compute its new spec.
+                    {Tree, [{OpN, erl_types:t_fun(arg_types(Args), erl_types:t_any())} | D1], true, CD1};
+                  false ->
+                    %% If it is not, it may be a closure.
+                    case sets:is_element(OpN, Closures) of
+                      true ->
+                        %% If it is, calculate its new spec.
+                        {Tree, D1, true, [{OpN, erl_types:t_fun(arg_types(Args), erl_types:t_any())} | CD1]};
+                      false->
+                        %% If it isn't leave the apply node as is.
+                        {Tree, D1, false, CD1}
+                    end
+                end
+            end;
+          _ ->
+            %% This shouldn't be reachable.
+            %% If we reach here it means that an apply was made to a variable,
+            %% that is not of the form {F, A}.
+            error("unhandled op")
+        end;
+      _ -> {Tree, D1, false, CD1}
+    end,
+  Change = C1 or C2 or (CurType =/= get_cerl_type(Tree1)),
+  {cerl:update_c_apply(Tree1, Op, Args), D2, Change, CD2, P1}.
+
+%% Similar to the logic of the apply node.
+%% It follows the same checks but disregards closures
+%% since they would be called through an apply node.
+pass_down_types_call(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType) ->
+  {Args, D1, C1, CD1, P1} = pass_down_types_all(cerl:call_args(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+  ModName = cerl:call_module(Tree),
+  Name = cerl:call_name(Tree),
+  Arity = length(cerl:call_args(Tree)),
+  {Tree1, D2, C2} =
+    case lists:all(fun has_type/1, Args) of
+      true ->
+        case cerl:is_literal(ModName) andalso cerl:is_literal(Name) of
+          true ->
+            OpN = {element(3, ModName), element(3, Name), Arity},
+            case dict:find(OpN, TSM) of
+              {ok, Specs} ->
+                case application_type(Specs, arg_types(Args)) of
+                  {ok, Type} ->
+                    {update_type(Tree, Type), D1, false};
+                  _ ->
+                    case sets:is_element(OpN, NoSpec) of
+                      true ->
+                        NewSpec = rewrite_spec(arg_types(Args), Specs),
+                        {Tree, [{OpN, NewSpec} | D1], true};
+                      false -> {Tree, D1, false}
+                    end
+                end;
+              error ->
+                case sets:is_element(OpN, NoSpec) of
+                  true ->
+                    {Tree, [{OpN, erl_types:t_fun(arg_types(Args), erl_types:t_any())} | D1], true};
+                  false ->
+                    {Tree, D1, false}
+                end
+            end;
+          _ -> throw("Unsupported call")
+        end;
+      _ -> {Tree, D1, false}
+    end,
+  Change = C1 or C2 or (CurType =/= get_cerl_type(Tree1)),
+  {cerl:update_c_call(Tree1, ModName, Name, Args), D2, Change, CD1, P1}.
+
+%% Handles case nodes. In case nodes we also have to annotate clauses that
+%% are unreachable using the type data with the annotation 'type_dependent_unreachable'.
+pass_down_types_case(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType) ->
+  %% Call recursively for argument and clauses.
+  {Arg, D1, C1, CD1, P1} = pass_down_types(cerl:case_arg(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+  {Clauses1, D2, C2, CD2, P2} = pass_down_types_all(cerl:case_clauses(Tree), TSM, Mod, get_cerl_type(Arg), NoSpec, Closures),
+  %% Then mark unreachable clauses.
+  Clauses = mark_unreachable_clauses(Clauses1, get_cerl_type(Arg), TSM, Arg),
+  Clauses2 = [Clause || Clause <- Clauses, not get_type_dependent_unreachable(Clause)],
+  %% The type of the case node is the union of all types of reachable clauses.
+  Type = 
+    case lists:all(fun has_type/1, Clauses2) of
+      true ->
+        T = arg_types(Clauses2),
+        case cuter_graphs:list_contains(notype, T) of
+          true -> notype;
+          false -> t_union(T)
+        end;
+      false ->
+        notype
+    end,
+  Change = C1 or C2 or (CurType =/= Type),
+  P = merge_all_dicts([P1, P2]),
+  {cerl:update_c_case(update_type(Tree, Type), Arg, Clauses), D1 ++ D2, Change, CD1 ++ CD2, P}.
+
+%% Handles clause nodes.
+pass_down_types_clause(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType) ->
+  %% Define a closure to map to all patterns of the clause.
+  %% This closure creates the symbol table containing all the variables
+  %% constrained by the guard, and calls unify_pattern/4 to create
+  %% the updated symbol table for the clause.
+  Fn = fun({Pat, AType}, V) ->
+           case V of
+             {ok, V1} ->
+               {A, TSMorT} = update_tsm_from_guard(Tree, V1, []),
+               case A of
+                 tsm ->
+                   unify_pattern(Pat, V1, TSMorT, AType);
+                 _ ->
+                   unify_pattern(Pat, V1, dict:new(), AType)
+               end;
+             {error, mismatch} -> {error, mismatch}
+           end
+       end,
+  %% Check if there are more than one pattern.
+  case length(cerl:clause_pats(Tree)) > 1 of
+    true ->
+      %% If there are, check if ArgType is a tuple.
+      case erl_types:t_is_tuple(ArgType) of
+        true ->
+          %% If it is, get the types of the elements of ArgType.
+          ATypes = erl_types:t_tuple_args(ArgType),
+          %% These should be as many as the patterns.
+          case length(ATypes) =:= length(cerl:clause_pats(Tree)) of
+            true ->
+              ArgTypes = ATypes;
+            false ->
+              ArgTypes = [notype || _ <- cerl:clause_pats(Tree)]
+          end;
+        false -> ArgTypes = [notype || _ <- cerl:clause_pats(Tree)]
+      end;
+    false -> ArgTypes = [ArgType]
+  end,
+  %% Check if ArgTypes have the same length as the patterns (check for just one pattern).
+  %% Then use Fn to create the new symbol table.
+  case length(ArgTypes) =/= length(cerl:clause_pats(Tree)) of
+    true -> 
+      TSMt = {error, arglen};
+    false ->
+      TSMt = lists:foldl(Fn, {ok, TSM}, lists:zip(cerl:clause_pats(Tree), ArgTypes))
+  end,
+  case TSMt of
+    {ok, TSMU} ->
+      TSM1 = TSMU;
+    {error, _} ->
+      TSM1 = TSM
+  end,
+  %% Use the new symbol table to pass down the types to all children and return normally.
+  {Pats, D1, C1, CD1, P1} = pass_down_types_all(cerl:clause_pats(Tree), TSM1, Mod, ArgType, NoSpec, Closures),
+  {Guard, D2, C2, CD2, P2} = pass_down_types(cerl:clause_guard(Tree), TSM1, Mod, ArgType, NoSpec, Closures),
+  {Body, D3, C3, CD3, P3} = pass_down_types(cerl:clause_body(Tree), TSM1, Mod, ArgType, NoSpec, Closures),
+  Change = C1 or C2 or C3 or (CurType =/= get_cerl_type(Body)),
+  D = lists:append([D1, D2, D3]),
+  CD = lists:append([CD1, CD2, CD3]),
+  P = merge_all_dicts([P1, P2, P3]),
+  {cerl:update_c_clause(update_type(Tree, get_cerl_type(Body)), Pats, Guard, Body), D, Change, CD, P}.
+
+%% Handles a fun node.
+pass_down_types_fun(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType) ->
+  %% Add the function variables to the symbol table.
+  TSM1 = put_vars(cerl:fun_vars(Tree), [erl_types:t_any() || _ <- cerl:fun_vars(Tree)], TSM),
+  %% Annotate them, we can since they are in the symbol table.
+  {Vars, _D1, _C1, _CD1, _P1} = pass_down_types_all(cerl:fun_vars(Tree), TSM1, Mod, ArgType, NoSpec, Closures),
+  %% Annotate the body.
+  {Body, D1, C1, CD1, P1} = pass_down_types(cerl:fun_body(Tree), TSM1, Mod, ArgType, NoSpec, Closures),
+  %% Create the new function type of the node.
+  Tree1 =
+    case has_type(Body) of
+      true ->
+        case get_cerl_type(Body) of
+          notype -> update_type(Tree, notype);
+          _ ->
+            Type = erl_types:t_fun([erl_types:t_any() || _ <- cerl:fun_vars(Tree)], get_cerl_type(Body)),
+            update_type(Tree, Type)
+        end;
+      _ -> update_type(Tree, notype)
+    end,
+  Change = C1 or (CurType =/= get_cerl_type(Tree1)),
+  {cerl:update_c_fun(Tree1, Vars, Body), D1, Change, CD1, P1}.
+
+%% Handles a let node.
+pass_down_types_let(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType) ->
+  %% Find the types of the assigned values to variables.
+  {Arg, D1, C1, CD1, P1} = pass_down_types(cerl:let_arg(Tree), TSM, Mod, ArgType, NoSpec, Closures),
+  %% Put the variables to the symbol table.
+  TSM1 = put_vars(cerl:let_vars(Tree), let_arg_types(Arg), TSM),
+  {Vars, D2, C2, CD2, P2} = pass_down_types_all(cerl:let_vars(Tree), TSM1, Mod, ArgType, NoSpec, Closures),
+  {Body, D3, C3, CD3, P3} = pass_down_types(cerl:let_body(Tree), TSM1, Mod, ArgType, NoSpec, Closures),
+  %% The type of a let node is the type of its body.
+  Tree1 =
+    case has_type(Body) of
+      true ->
+        update_type(Tree, get_cerl_type(Body));
+      false ->
+        update_type(Tree, notype)
+    end,
+  Change = C1 or C2 or C3 or (CurType =/= get_cerl_type(Tree1)),
+  D = lists:append([D1, D2, D3]),
+  CD = lists:append([CD1, CD2, CD3]),
+  P = merge_all_dicts([P1, P2, P3]),
+  {cerl:update_c_let(Tree1, Vars, Arg, Body), D, Change, CD, P}.
+
+%% Handles a letrec node.
+%% Since this node introduces closures, we need to do a fix-point computation
+%% Similar to the top one for all functions. That is because closures initially
+%% don't have a signature since the programmer does not provide one. They also
+%% can be recursive in case they are compiler generated for list comprehensions.
+pass_down_types_letrec(Tree, TSM, Mod, ArgType, NoSpec, Closures, CurType) ->
+  {Names, Funsb} = lists:unzip(cerl:letrec_defs(Tree)),
+  FunNames = [cerl:var_name(Name) || Name <- Names],
+  FunNames1 = sets:from_list([{Mod, F, A} || {F, A} <- FunNames]),
+  %% Add the new closures to the set of closures.
+  NewClosures = sets:union(Closures, FunNames1),
+  %% Do the fix-point computation.
+  {Funs, Body, D, C, CD, TSM1} = pass_down_types_letrec_fix(Names, Funsb, cerl:letrec_body(Tree), TSM, Mod, ArgType, NoSpec, NewClosures),
+  %% Filter out all functions that are introduced in other letrec ndoes to create
+  FilterFun = fun(Key, _Value) -> sets:is_element(Key, FunNames1) end,
+  %% The peristence of the closures in this letrec node.
+  Persistence = dict:filter(FilterFun, TSM1),
+  Change = C or (CurType =/= get_cerl_type(Body)),
+  %% The type of the letrec node is the type of its body.
+  {cerl:update_c_letrec(update_type(Tree, get_cerl_type(Body)), lists:zip(Names, Funs), Body), D, Change, CD, Persistence}.
+
+%% Fix point computation for letrec nodes.
+pass_down_types_letrec_fix(Names, Funsb, Body, TSM, Mod, ArgType, NoSpec, Closures) ->
+  FunNames1 = [cerl:var_name(Name) || Name <- Names],
+  FunNames2 = [{Mod, F, A} || {F, A} <- FunNames1],
+  FunNames = sets:from_list(FunNames2),
+  %% Do a pass through the functions.
+  {Funs, D1, C1, CD1} = pass_down_types_letrec_fix_pass(FunNames2, Funsb, TSM, Mod, ArgType, NoSpec, Closures, []),
+  %% Do a pass through the body.
+  {Body1, D2, C2, CD2, _P2} = pass_down_types(Body, TSM, Mod, ArgType, NoSpec, Closures),
+  CD = CD1 ++ CD2,
+  %% Find all detected closure calls to closures that do not have yet a signature
+  %% or need their signature updated that belong to this letrec node.
+  RelevantCD = [D || {OpN, _NewSpec}=D <- CD, sets:is_element(OpN, FunNames)],
+  %% If there are none, we are done, else we continue the fix-point.
+  case length(RelevantCD) of
+    0 ->
+      RestCD = [D || {OpN, _NewSpec}=D <- CD, not sets:is_element(OpN, FunNames)],
+      {Funs, Body1, D1 ++ D2, C1 or C2, RestCD, TSM};
+    _ ->
+      {TSM1, _} = update_from_detected(RelevantCD, TSM, []),
+      pass_down_types_letrec_fix(Names, Funs, Body1, TSM1, Mod, ArgType, NoSpec, Closures)
+  end.
+
+%% Performs a pass through the functions introduced in a letrec node.
+pass_down_types_letrec_fix_pass([], _Funsb, _TSM, _Mod, _ArgType, _NoSpec, _Closures, Acc) ->
+  {Funs, D, C, CD, _P} = unzip5(Acc),
+  {lists:reverse(Funs), lists:append(D), lists:foldl(fun erlang:'or'/2, false, C), lists:append(CD)};
+pass_down_types_letrec_fix_pass([Name|Names], [Funb|Funsb], TSM, Mod, ArgType, NoSpec, Closures, Acc) ->
+  case dict:find(Name, TSM) of
+    {ok, [Spec]} ->
+      TSM1 = put_vars(cerl:fun_vars(Funb), erl_types:t_fun_args(Spec), TSM);
+    error ->
+      TSM1 = TSM
+  end,
+  {Args, _, _, _, _} = pass_down_types_all(cerl:fun_vars(Funb), TSM1, Mod, ArgType, NoSpec, Closures),
+  {Body, D, C, CD, P} = pass_down_types(cerl:fun_body(Funb), TSM1, Mod, ArgType, NoSpec, Closures),
+  Fun = cerl:update_c_fun(Funb, Args, Body),  
+  pass_down_types_letrec_fix_pass(Names, Funsb, TSM, Mod, ArgType, NoSpec, Closures, [{Fun, D, C, CD, P}|Acc]).
+
+%% Wrapper to call pass_down_types/6 to a list of nodes.
+pass_down_types_all(Trees, TSM, Mod, ArgType, NoSpec, Closures) ->
+  R = lists:map(fun(A) -> pass_down_types(A, TSM, Mod, ArgType, NoSpec, Closures) end, Trees),
+  {NewTrees, AllDetected, Changes, ClosuresDetected, Persistence} = unzip5(R),
+  {NewTrees, lists:append(AllDetected), lists:foldl(fun erlang:'or'/2, false, Changes), lists:append(ClosuresDetected), merge_all_dicts(Persistence)}.
+
+%% Unzips a list of tuples of length 5.
+unzip5(L) -> unzip5(L, [], [], [], [], []).
+
+unzip5([], Acc1, Acc2, Acc3, Acc4, Acc5) -> 
+  {lists:reverse(Acc1),
+   lists:reverse(Acc2),
+   lists:reverse(Acc3),
+   lists:reverse(Acc4),
+   lists:reverse(Acc5)};
+unzip5([{A, B, C, D, E}|Rest], Acc1, Acc2, Acc3, Acc4, Acc5) ->
+  unzip5(Rest, [A|Acc1], [B|Acc2], [C|Acc3], [D|Acc4], [E|Acc5]).
+
+%% Rewrites a function signature with updated argument types.
+rewrite_spec(ArgTypes, [Spec]) ->
+  SupArgs = fun({A, B}) -> erl_types:t_sup(A, B) end,
+  ArgTypes1 = lists:map(SupArgs, lists:zip(ArgTypes, erl_types:t_fun_args(Spec))),
+  erl_types:t_fun(ArgTypes1, erl_types:t_fun_range(Spec)).
+
+%% ===========================
+%% Marking unreachable clauses
+%% ===========================
+
+%% This is the entry point to the logic that marks the unreachable clauses of a case.
+%% Arguments:
+%% - Clauses: List of cerl nodes of type clause.
+%% - ArgType: The type of the case argument these clauses belong to.
+%% - TSM: Symbol table.
+%% - Arg: Case argument.
+%% Returns:
+%% The list of clauses annotated with 'type_dependent_unreachable' if they can't be reached.
+mark_unreachable_clauses(Clauses, ArgType, TSM, Arg) ->
+  %% Check if Arg is a values node to create the Argument list correctly.
+  case cerl:type(Arg) =:= values of
+    true -> ArgList = cerl:values_es(Arg);
+    false -> ArgList = [Arg]
+  end,
+  %% If we haven't computed a type for the argument,
+  %% we can not know if a clause is unreachable, so
+  %% just return clauses as they are.
+  case ArgType =:= notype of
+    false -> mark_unreachable_clauses(Clauses, ArgType, TSM, ArgList, []);
+    true -> Clauses
+  end.
+
+%% Tail-recursive so reverse the clauses when returning to maintain their order.
+mark_unreachable_clauses([], _, _, _, NewClauses) -> lists:reverse(NewClauses);
+mark_unreachable_clauses([Clause|Clauses], ArgType, TSM, Arg, NewClauses) ->
+  Pats =  cerl:clause_pats(Clause),
+  %% If the ArgType is None, we have subtracted everything from the original argument type.
+  %% This means that no further clauses can be reached, including this one.
+  NewClause =
+    case erl_types:t_is_none(ArgType) of
+      true -> mark_as_unreachable(Clause);
+      false -> mark_as_reachable(Clause)
+    end,
+  %% Closure to try to subtract two types, and just return the first one
+  %% intact in the case of failure.
+  SafeSub = fun(A, B) ->
+                try erl_types:t_subtract(A, B) of
+                  T -> T
+                catch
+                  _:_ -> A
+                end
+            end,
+  %% Update the symbol table from the clause guard.
+  {A, TSMorT} = update_tsm_from_guard(Clause, TSM, Arg),
+  %% Distinguish between the return values of update_tsm_from_guard/3.
+  case A of
+    {argtype, ArgName} ->
+      %% We only have a constraint for an argument
+      PatTypes1 = lists:map(fun (X) -> t_from_pattern(X, TSM, dict:new()) end, Pats),
+      %% Gather the patterns that have a type and convert them to erl_types.
+      PatTypes = [PatType || PatType <- PatTypes1, PatType =/= notype],
+      %% Check if we could do that for all of them.
+      case length(PatTypes) =:= length(Arg) of
+        true ->
+          %% We could, so replace the variable with its constraint in the patterns.
+          %% And then make the new type by subtracting to the current ArgType.
+          PatTypes2 = replace_guard_type(Arg, ArgName, PatTypes, TSMorT),
+          case length(PatTypes) > 1 of
+            true ->
+              PatTypes3 = erl_types:t_tuple(PatTypes2),
+              T = SafeSub(ArgType, PatTypes3);
+            false ->
+              PatTypes3 = hd(PatTypes2),
+              T = SafeSub(ArgType, PatTypes3)
+          end;
+        false ->
+          T = ArgType
+      end;
+    tsm ->
+      %% We have an updated symbol table.
+      %% Do the same as the previous case using the new symbol table.
+      PatTypes1 = lists:map(fun (X) -> t_from_pattern(X, TSM, TSMorT) end, Pats),
+      PatTypes = [PatType || PatType <- PatTypes1, PatType =/= notype],
+      case length(PatTypes) =:= length(Arg) of
+        true ->
+          case length(PatTypes) > 1 of
+            true ->
+              PatTypes3 = erl_types:t_tuple(PatTypes),
+              T = SafeSub(ArgType, PatTypes3);
+            false ->
+              PatTypes3 = hd(PatTypes),
+              T = SafeSub(ArgType, PatTypes3)
+          end;
+        false ->
+          T = ArgType
+      end;
+    invalid ->
+      T = ArgType
+  end,
+  mark_unreachable_clauses(Clauses, T, TSM, Arg, [NewClause|NewClauses]).
+
+%% Replaces an argument with the type it is constrained to in the patterns.
+replace_guard_type([], _ArgName, [], _TSMorT) -> [];
+replace_guard_type([Arg|Args], ArgName, [PatType|PatTypes], TSMorT) -> 
+  case cerl:type(Arg) =:= var of
+    true ->
+      case cerl:var_name(Arg) =:= ArgName of
+        true ->
+          [TSMorT|PatTypes];
+        false ->
+          [PatType|replace_guard_type(Args, ArgName, PatTypes, TSMorT)]
+      end;
+    false ->
+      [PatType|replace_guard_type(Args, ArgName, PatTypes, TSMorT)]
+  end.
+
+%% A valid guard is a guard we can currently parse to extract useful information
+%% that helps us locate the unreachable clauses in a case construct.
+valid_guard(Clause, TSM, ArgList) ->
+  Guard = cerl:clause_guard(Clause),
+  case cerl:type(Guard) of
+    literal when element(3, Guard) =:= true -> true;
+    call ->
+      Args = cerl:call_args(Guard),
+      case get_call_mfa(Guard) of
+        {erlang, is_integer, 1} -> is_unknown_var(hd(Args), TSM, ArgList);
+        {erlang, is_atom, 1} -> is_unknown_var(hd(Args), TSM, ArgList);
+        {erlang, is_function, 1} -> is_unknown_var(hd(Args), TSM, ArgList);
+        {erlang, is_function, 2} ->
+          C1 = is_unknown_var(hd(Args), TSM, ArgList),
+          C2 = cerl:type(lists:nth(2, Args)) =:= literal,
+          C1 or C2;
+        _ -> false
+      end;
+    'try' -> 
+      TryArg = cerl:try_arg(Guard),
+      case cerl:type(TryArg) of 
+        'let' ->
+          case length(cerl:let_vars(TryArg)) =:= 1 of
+            true ->
+              LetVar = hd(cerl:let_vars(TryArg)),
+              LetBody = cerl:let_body(TryArg),
+              LetArg = cerl:let_arg(TryArg),
+              case cerl:type(LetArg) of
+                'call' ->
+                  case get_call_mfa(LetArg) of
+                    {erlang, is_function, 2} ->
+                      case cerl:type(LetBody) of
+                        'call' ->
+                          case is_right_call(LetBody, LetVar) of
+                            true ->
+                              is_unknown_var(hd(cerl:call_args(LetArg)), TSM, ArgList);
+                            false -> false
+                          end;
+                        _ -> false
+                      end;
+                    _ -> false
+                  end;
+                _ -> false
+              end;
+            false -> false
+          end;
+        _ -> false
+      end;
+    _ -> false
+  end.
+
+%% Returns the Mfa called from a guard.
+get_call_mfa(Guard) ->
+  ModName = cerl:call_module(Guard),
+  Name = cerl:call_name(Guard),
+  Arity = length(cerl:call_args(Guard)),
+  case cerl:type(ModName) =:= literal andalso cerl:type(Name) =:= literal of
+    true -> {element(3, ModName), element(3, Name), Arity};
+    false -> unmatched
+  end.
+
+%% Returns whether X is a variable that is not in the symbol table or
+%% in the arguent list of a case construct.
+is_unknown_var(X, TSM, ArgList) ->
+  case cerl:type(X) of
+    var ->
+      ArgVarNames = [cerl:var_name(Var) || Var <- ArgList, cerl:type(Var) =:= var],
+      case dict:find(cerl:var_name(X), TSM) of
+        {ok, _} -> cuter_graphs:list_contains(cerl:var_name(X), ArgVarNames);
+        error -> true
+      end;
+    _ -> false
+  end.
+
+%% A 'right' call is a call we support for guards.
+is_right_call(Call, LetVar) ->
+  case get_call_mfa(Call) =:= {erlang, '=:=', 2} of
+    true ->
+      [Arg1, Arg2] = cerl:call_args(Call),
+      case cerl:type(Arg1) =:= var andalso cerl:type(Arg2) =:= literal of
+        true -> cerl:var_name(LetVar) =:= cerl:var_name(Arg1) andalso element(3, Arg2) =:= true;
+        false -> false
+      end;
+    false -> false
+  end.
+
+%% This function looks at the guard of a clause.
+%% If the guard is of the form is_'type'(X), it returns the constraint
+%% that variable X has the type 'type'.
+update_tsm_from_guard(Clause, TSM, ArgList) ->
+  case valid_guard(Clause, TSM, ArgList) of
+    true ->
+      Guard = cerl:clause_guard(Clause),
+      case cerl:type(Guard) of
+        literal when element(3, Guard) =:= true -> {tsm, dict:new()};
+        call ->
+          Args = cerl:call_args(Guard),
+          case get_call_mfa(Guard) of
+            {erlang, is_integer, 1} ->
+              update_tsm_from_guard_helper(Args, ArgList, erl_types:t_integer());
+            {erlang, is_atom, 1} ->
+              update_tsm_from_guard_helper(Args, ArgList, erl_types:t_atom());
+            {erlang, is_function, 1} ->
+              update_tsm_from_guard_helper(Args, ArgList, erl_types:t_fun());
+            {erlang, is_function, 2}->
+              Arity = element(3, lists:nth(2, Args)),
+              update_tsm_from_guard_helper(Args, ArgList, erl_types:t_fun(Arity, erl_types:t_any()))
+          end;
+        'try' ->
+          TryArg = cerl:try_arg(Guard),
+          LetArg = cerl:let_arg(TryArg),
+          Args = cerl:call_args(LetArg),
+          case get_call_mfa(LetArg) of
+            {erlang, is_function, 2} ->
+              Arity = element(3, lists:nth(2, Args)),
+              update_tsm_from_guard_helper(Args, ArgList, erl_types:t_fun(Arity, erl_types:t_any()))
+          end
+      end;
+    false ->
+      {invalid, none}
+  end.
+
+%% Decides whether to return a new symbol table,
+%% or just a variable constraint.
+update_tsm_from_guard_helper(Args, ArgList, Type) ->
+  FunArgName = cerl:var_name(hd(Args)),
+  ArgVarNames = [cerl:var_name(Var) || Var <- ArgList, cerl:type(Var) =:= var],
+  case cuter_graphs:list_contains(FunArgName, ArgVarNames) of
+    true -> {{argtype, FunArgName}, Type};
+    _ -> {tsm, dict:store(FunArgName, Type, dict:new())}
+  end.
+
+%% Fetches the 'type_dependent_unreachable' annotation out of an annotation list.
+get_ann_type_dependent_unreachable([]) -> false;
+get_ann_type_dependent_unreachable([Hd|Tl]) ->
+  case Hd of
+    type_dependent_unreachable ->
+      true;
+    _ ->
+      get_ann_type_dependent_unreachable(Tl)
+  end.
+
+%% Fetches the 'type_dependent_unreachable' annotation of a cerl node.
+-spec get_type_dependent_unreachable(cerl:cerl()) -> boolean().
+get_type_dependent_unreachable(T) -> get_ann_type_dependent_unreachable(cerl:get_ann(T)).
+
+%% Merges all dictionaries in a list.
+%% It hypothesizes that no two keys are the same.
+merge_all_dicts(D) ->
+  F = fun(_Key, Value1, _Value2) -> Value1 end,
+  F1 = fun(D1, D2) -> dict:merge(F, D1, D2) end,
+  lists:foldl(F1, dict:new(), D).
diff --git a/src/cuter_type_dependent_functions.erl b/src/cuter_type_dependent_functions.erl
new file mode 100644
index 00000000..2df74067
--- /dev/null
+++ b/src/cuter_type_dependent_functions.erl
@@ -0,0 +1,353 @@
+-module(cuter_type_dependent_functions).
+-export([original_tsm/0]).
+
+%% Returns a dictionary with:
+%% Keys: Mfas of built-in functions
+%% Values: List of signatures of these functions.
+-spec original_tsm() -> dict:dict().
+original_tsm() ->
+  TSM = dict:from_list(
+	  [
+	   {
+	    {erlang,'+',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,number,{int_rng,1,pos_inf},integer},
+		 {c,number,{int_rng,1,pos_inf},integer}],
+		unknown},
+	       {c,number,{int_rng,1,pos_inf},integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,
+		[{c,number,any,integer},{c,number,any,integer}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,
+		[{c,number,any,unknown},{c,number,any,unknown}],
+		unknown},
+	       {c,number,any,unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'-',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,number,any,integer},{c,number,any,integer}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,
+		[{c,number,any,unknown},{c,number,any,unknown}],
+		unknown},
+	       {c,number,any,unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'*',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,number,{int_rng,1,pos_inf},integer},
+		 {c,number,{int_rng,1,pos_inf},integer}],
+		unknown},
+	       {c,number,{int_rng,1,pos_inf},integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,
+		[{c,number,any,integer},{c,number,any,integer}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,
+		[{c,number,any,unknown},{c,number,any,unknown}],
+		unknown},
+	       {c,number,any,unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'rem',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,number,any,integer},
+		 {c,number,{int_rng,1,pos_inf},integer}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,
+		[{c,number,any,integer},
+		 {c,number,{int_rng,neg_inf,-1},integer}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'div',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,number,any,integer},
+		 {c,number,{int_rng,1,pos_inf},integer}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,
+		[{c,number,any,integer},
+		 {c,number,{int_rng,neg_inf,-1},integer}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'=:=',2},
+	    [{c,function,
+	      [{c,product,[any,any],unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,length,1},
+	    [{c,function,
+	      [{c,product,
+		[{c,list,[any,{c,nil,[],unknown}],unknown}],
+		unknown},
+	       {c,number,{int_rng,0,pos_inf},integer}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,tuple_size,1},
+	    [{c,function,
+	      [{c,product,[{c,tuple,any,{any,any}}],unknown},
+	       {c,number,{int_rng,0,pos_inf},integer}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,float,1},
+	    [{c,function,
+	      [{c,product,[{c,number,any,unknown}],unknown},
+	       {c,number,any,float}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,list_to_tuple,1},
+	    [{c,function,
+	      [{c,product,
+		[{c,list,[any,{c,nil,[],unknown}],unknown}],
+		unknown},
+	       {c,tuple,any,{any,any}}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,tuple_to_list,1},
+	    [{c,function,
+	      [{c,product,[{c,tuple,any,{any,any}}],unknown},
+	       {c,list,[any,{c,nil,[],unknown}],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,int_to_char,1},
+	    [{c,function,
+	      [{c,product,
+		[{c,number,{int_set,[0,1,2,3,4,5,6,7,8,9]},integer}],
+		unknown},
+	       {c,number,{int_set,"0123456789"},integer}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,integer_to_list,1},
+	    [{c,function,
+	      [{c,product,[{c,number,any,integer}],unknown},
+	       {c,list,
+		[{c,number,{int_set,"-0123456789"},integer},
+		 {c,nil,[],unknown}],
+		nonempty}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,list_to_integer,1},
+	    [{c,function,
+	      [{c,product,
+		[{c,list,
+		  [{c,number,{int_set,"+-0123456789"},integer},
+		   {c,nil,[],unknown}],
+		  nonempty}],
+		unknown},
+	       {c,number,any,integer}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,abs,1},
+	    [{c,function,
+	      [{c,product,[{c,number,any,integer}],unknown},
+	       {c,number,{int_rng,0,pos_inf},integer}],
+	      unknown},
+	     {c,function,
+	      [{c,product,[{c,number,any,float}],unknown},
+	       {c,number,any,float}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,trunc,1},
+	    [{c,function,
+	      [{c,product,[{c,number,any,unknown}],unknown},
+	       {c,number,any,integer}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'not',1},
+	    [{c,function,
+	      [{c,product,[{c,atom,[false,true],unknown}],unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'and',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,atom,[false,true],unknown},
+		 {c,atom,[false,true],unknown}],
+		unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'andalso',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,atom,[false,true],unknown},
+		 {c,atom,[false,true],unknown}],
+		unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'or',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,atom,[false,true],unknown},
+		 {c,atom,[false,true],unknown}],
+		unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'orelse',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,atom,[false,true],unknown},
+		 {c,atom,[false,true],unknown}],
+		unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'xor',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,atom,[false,true],unknown},
+		 {c,atom,[false,true],unknown}],
+		unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'=/=',2},
+	    [{c,function,
+	      [{c,product,[any,any],unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'==',2},
+	    [{c,function,
+	      [{c,product,[any,any],unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'/=',2},
+	    [{c,function,
+	      [{c,product,[any,any],unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,hd,1},
+	    [{c,function,
+	      [{c,product,
+		[{c,list,[any,{c,nil,[],unknown}],nonempty}],
+		unknown},
+	       any],
+	      unknown}]
+	   },
+	   {
+	    {erlang,tl,1},
+	    [{c,function,
+	      [{c,product,
+		[{c,list,[any,{c,nil,[],unknown}],nonempty}],
+		unknown},
+	       any],
+	      unknown}]
+	   },
+	   {
+	    {erlang,'++',2},
+	    [{c,function,
+	      [{c,product,
+		[{c,list,[any,{c,nil,[],unknown}],unknown},
+		 {c,list,[any,{c,nil,[],unknown}],unknown}],
+		unknown},
+	       {c,list,[any,{c,nil,[],unknown}],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {lists,reverse,2},
+	    [{c,function,
+	      [{c,product,
+		[{c,list,[any,{c,nil,[],unknown}],unknown},
+		 {c,list,[any,{c,nil,[],unknown}],unknown}],
+		unknown},
+	       {c,list,[any,{c,nil,[],unknown}],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {lists,member,2},
+	    [{c,function,
+	      [{c,product,
+		[any,{c,list,[any,{c,nil,[],unknown}],unknown}],
+		unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,is_integer,1},
+	    [{c,function,
+	      [{c,product,[any],unknown},{c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,is_atom,1},
+	    [{c,function,
+	      [{c,product,[any],unknown},{c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,is_function,1},
+	    [{c,function,
+	      [{c,product,[any],unknown},{c,atom,[false,true],unknown}],
+	      unknown}]
+	   },
+	   {
+	    {erlang,is_function,2},
+	    [{c,function,
+	      [{c,product,
+		[any,{c,number,{int_rng,1,255},integer}],
+		unknown},
+	       {c,atom,[false,true],unknown}],
+	      unknown}]
+	   }
+	  ]
+	 ),
+  TSM.
diff --git a/src/cuter_types.erl b/src/cuter_types.erl
index 6eb96199..74d41d24 100644
--- a/src/cuter_types.erl
+++ b/src/cuter_types.erl
@@ -8,7 +8,7 @@
 -export([params_of_t_function_det/1, ret_of_t_function/1, atom_of_t_atom_lit/1,
 	 integer_of_t_integer_lit/1, elements_type_of_t_list/1,
 	 elements_type_of_t_nonempty_list/1, elements_types_of_t_tuple/1,
-   assocs_of_t_map/1, elements_types_of_t_union/1, bounds_of_t_range/1,
+	 assocs_of_t_map/1, elements_types_of_t_union/1, bounds_of_t_range/1,
 	 segment_size_of_bitstring/1, is_generic_function/1,
 	 name_of_t_userdef/1]).
 
@@ -23,6 +23,10 @@
 -export([erl_type_deps_map/2, get_type_name_from_type_dep/1,
 	 get_type_from_type_dep/1, unique_type_name/3]).
 
+-export([specs_as_erl_types/1]).
+
+-export([mfa_to_string/1, are_sets_equal/2]).
+
 -export_type([erl_type/0, erl_spec_clause/0, erl_spec/0, stored_specs/0,
 	      stored_types/0, stored_spec_value/0, t_range_limit/0]).
 -export_type([erl_type_dep/0, erl_type_deps/0]).
@@ -737,11 +741,11 @@ unify_deps(Types) ->
 %% define an intermediate representation solely for specs.
 %% ============================================================================
 
--spec retrieve_specs([cuter_cerl:spec_info()]) -> stored_specs().
+-spec retrieve_specs([cuter_cerl:cerl_spec_form()]) -> stored_specs().
 retrieve_specs(SpecAttrs) ->
   lists:foldl(fun process_spec_attr/2, dict:new(), SpecAttrs).
 
--spec process_spec_attr(cuter_cerl:spec_info(), stored_specs()) -> stored_specs().
+-spec process_spec_attr(cuter_cerl:cerl_spec_form(), stored_specs()) -> stored_specs().
 process_spec_attr({FA, Specs}, Processed) ->
   Xs = [t_spec_from_form(Spec) || Spec <- Specs],
   dict:store(FA, Xs, Processed).
@@ -991,7 +995,7 @@ simplify_constraints(Constraints, CurrModule, Env, Visited, Conf) ->
     end,
   lists:foldl(F, Env, Constraints).
 
--spec simplify(raw_type(), atom(), type_var_env(), ordsets:ordset(stored_spec_key()), parse_conf()) -> raw_type().
+-spec simplify(raw_type(), module(), type_var_env(), ordsets:ordset(stored_spec_key()), parse_conf()) -> raw_type().
 %% fun
 simplify(#t{kind = ?function_tag, rep = {Params, Ret, Constraints}}=Raw, CurrModule, Env, Visited, Conf) ->
   Env1 = simplify_constraints(Constraints, CurrModule, Env, Visited, Conf),
@@ -1115,8 +1119,8 @@ lookup_in_env(Key, Env) ->
   end.
 
 %% ============================================================================
-%% Traverse a pre-processed spec or type and find its remote dependencies, aka
-%% the remote types that it contains.
+%% Traverses a pre-processed spec or type and finds its remote dependencies,
+%% i.e., the remote types that it contains.
 %% ============================================================================
 
 %% Finds the remote dependencies of a spec.
@@ -1132,7 +1136,7 @@ find_remote_deps_of_type(Type, LocalTypesCache) ->
   ordsets:to_list(Deps).
 
 %% ----------------------------------------------------------------------------
-%% Traverse a type and collect its remote dependencies.
+%% Traverses a type and collects its remote dependencies.
 %% Performing case analysis on the type of the type node.
 %% ----------------------------------------------------------------------------
 
@@ -1213,3 +1217,291 @@ get_type_name_from_type_dep({Name, _Type}) ->
 -spec get_type_from_type_dep(erl_type_dep()) -> erl_type().
 get_type_from_type_dep({_Name, Type}) ->
   Type.
+
+%% ----------------------------------------------------------------------------
+%% Compute the erl_types:erl_type() representation of type specifications.
+%% ----------------------------------------------------------------------------
+
+-define(CUTER_RECORD_TYPE_PREFIX, "__cuter_record_type__").
+
+%% Returns the specs of the given kmodules in their erl_types representation.
+-spec specs_as_erl_types([cuter_cerl:kmodule()]) -> dict:dict(mfa(), [erl_types:erl_type()]).
+specs_as_erl_types(Kmodules) ->
+  %% Initialize an openset with all the types that have not yet been
+  %% converted from a form to its erl_types representation.
+  Openset = initial_openset_of_types(Kmodules),
+  Exported = sets:union([cuter_cerl:kmodule_exported_types(KM) || KM <- Kmodules]),
+  Specs = specs_as_erl_types_fix(Kmodules, Exported, Openset),
+  %% Gather all specs available in the modules.
+  AllFunSpecs = lists:append([[{{cuter_cerl:kmodule_name(Kmodule), F, A}, S} || {{F, A}, S} <- cuter_cerl:kmodule_spec_forms(Kmodule)] || Kmodule <- Kmodules]),
+  ReportUnhandled =
+    fun({MFA, Form}) ->
+	case dict:find(MFA, Specs) of
+	  {ok, ErlType} ->
+	    case length(ErlType) =:= length(Form) of
+	      false -> warn_unhandled_spec(MFA);
+	      true  -> ok
+	    end
+	end
+    end,
+  %% Report which specs couldn't be succesfully converted to an erl_type.
+  lists:foreach(ReportUnhandled, AllFunSpecs),
+  Specs.
+
+initial_openset_of_types(Kmodules) ->
+  initial_openset_of_types(Kmodules, sets:new()).
+
+initial_openset_of_types([], Openset) ->
+  Openset;
+initial_openset_of_types([KM|KMs], Openset) ->
+  TypeForms = extract_type_definitions(KM),
+  M = cuter_cerl:kmodule_name(KM),
+  Ts = sets:from_list([{M, TName, length(Vars)} || {_L, {TName, _T, Vars}} <- TypeForms]),
+  initial_openset_of_types(KMs, sets:union(Openset, Ts)).
+
+%% Converts all the function specifications of the kmodules until fixpoint.
+specs_as_erl_types_fix(Kmodules, Exported, Openset) ->
+  RecDict = ets:new(recdict, []),  %% Needed for erl_types:t_from_form/6.
+  R = specs_as_erl_types_fix(Kmodules, Exported, RecDict, Openset, dict:new()),
+  ets:delete(RecDict),
+  R.
+
+specs_as_erl_types_fix(KMs, Exported, RecDict, Openset, GatheredSpecs) ->
+  {Openset1, GatheredSpecs1} = specs_as_erl_types_fix_pass(KMs, Exported, RecDict, Openset, GatheredSpecs),
+  case are_sets_equal(Openset, Openset1) of
+    true -> GatheredSpecs1;
+    false -> specs_as_erl_types_fix(KMs, Exported, RecDict, Openset1, GatheredSpecs1)
+  end.
+
+%% Iterates through each kmodule and converts function specifications into their
+%% erl_types representation.
+specs_as_erl_types_fix_pass([], _Exported, _RecDict, Openset, GatheredSpecs) ->
+  {Openset, GatheredSpecs};
+specs_as_erl_types_fix_pass([KM|Rest]=KMs, Exported, RecDict, Openset, GatheredSpecs) ->
+  Mod = cuter_cerl:kmodule_name(KM),
+  ModOpenset = sets:filter(fun({M, _T, _A}) -> M =:= Mod end, Openset),
+  {NewModOpenset, ComputedSpecs} = module_specs_as_erl_types(KM, Exported, RecDict),
+  GatheredSpecs1 = update_gathered_specs(ComputedSpecs, GatheredSpecs),
+  case are_sets_equal(NewModOpenset, ModOpenset) of
+    %% The openset of the module has reached a fixpoint.
+    true ->
+      specs_as_erl_types_fix_pass(Rest, Exported, RecDict, Openset, GatheredSpecs1);
+    %% If the openset of the module has changed, we want to re-run the
+    %% computation.  This can happen when a type depends on a type
+    %% that is defined later in the code, or for mutually recursive types.
+    false ->
+      OtherModsOpenset = sets:subtract(Openset, ModOpenset),
+      specs_as_erl_types_fix_pass(KMs, Exported, RecDict, sets:union(NewModOpenset, OtherModsOpenset), GatheredSpecs1)
+  end.
+
+update_gathered_specs([], GatheredSpecs) -> GatheredSpecs;
+update_gathered_specs([{Mfa, Spec}|More], GatheredSpecs) ->
+  GatheredSpecs1 = dict:store(Mfa, Spec, GatheredSpecs),
+  update_gathered_specs(More, GatheredSpecs1).
+
+%% Computes the specs of a kmodule as erl_types.
+%% Returns the computes specs, and the types that were not computed yet.
+module_specs_as_erl_types(Kmodule, Exported, RecDict) ->
+  %% Run one pass that computes the types in the module.
+  ModOpenset = update_recdict_for_module_types(Kmodule, Exported, RecDict),
+  %% Compute the specs based on the potentially updated types.
+  SpecForms = cuter_cerl:kmodule_spec_forms(Kmodule),
+  Specs = [spec_form_as_erl_types(SF, Kmodule, Exported, RecDict) || SF <- SpecForms],
+  {ModOpenset, Specs}.
+
+update_recdict_for_module_types(Kmodule, Exported, RecDict) ->
+  TypeForms = extract_type_definitions(Kmodule),
+  M = cuter_cerl:kmodule_name(Kmodule),
+  update_recdict_from_type_forms(M, RecDict, Exported, TypeForms).
+
+spec_form_as_erl_types({{F, A}, Spec}, Kmodule, Exported, RecDict) ->
+  NormalizedSpec = replace_records_in_spec(transform_bounded_funs_in_spec(Spec)),
+  Mfa = {cuter_cerl:kmodule_name(Kmodule), F, A},
+  Converted = normalized_spec_form_as_erl_types(NormalizedSpec, Mfa, Exported, RecDict),
+  {Mfa, Converted}.
+
+%% Converts as many types in M as possible to their erl_types representation.
+%% Every succesful conversion is added to RecDict.
+%% We return the types that could not be converted, i.e. the openset.
+update_recdict_from_type_forms(M, RecDict, Exported, TypeForms) ->
+  Fn = fun ({L, {TName, T, TVars}}, Acc) ->
+	   A = length(TVars),
+	   Mta = {M, TName, A},
+	   Vs = [V || {var, _, V} <- TVars],
+	   case try_convert_type_to_erl_types(Mta, T, Exported, RecDict) of
+	     error -> sets:add_element(Mta, Acc);
+	     {ok, T1} ->
+	       VT =
+		 case ets:lookup(RecDict, M) of
+		   [{M, OVT}] -> OVT;
+		   [] -> maps:new()
+		 end,
+	       NVT = maps:put({'type', TName, A}, {{M, {atom_to_list(M) ++ ".erl", L}, T, Vs}, T1}, VT),
+	       ets:insert(RecDict, {M, NVT}),
+	       Acc
+	   end
+       end,
+  lists:foldl(Fn, sets:new(), TypeForms).
+
+try_convert_type_to_erl_types(Mta, T, Exported, RecDict) ->
+  VT = erl_types:var_table__new(),
+  Cache = erl_types:cache__new(),
+  try erl_types:t_from_form(T, Exported, {'type', Mta}, RecDict, VT, Cache) of
+    {T1, _C} -> {ok, T1}
+  catch
+    _:_ -> error
+  end.
+
+%% Converts a spec without bounded funs and records to its erl_types
+%% representation.
+normalized_spec_form_as_erl_types(Spec, Mfa, TypeForms, RecDict) ->
+  normalized_spec_form_as_erl_types(Spec, Mfa, TypeForms, RecDict, []).
+
+normalized_spec_form_as_erl_types([], _Mfa, _TypeForms, _RecDict, Acc) ->
+  lists:reverse(Acc);
+normalized_spec_form_as_erl_types([FC|FCs], Mfa, TypeForms, RecDict, Acc) ->
+  VT = erl_types:var_table__new(),
+  Cache = erl_types:cache__new(),
+  try erl_types:t_from_form(FC, TypeForms, {'spec', Mfa}, RecDict, VT, Cache) of
+    {S, _C} ->
+      normalized_spec_form_as_erl_types(FCs, Mfa, TypeForms, RecDict, [S|Acc])
+  catch
+    _:_ ->
+      normalized_spec_form_as_erl_types(FCs, Mfa, TypeForms, RecDict, Acc)
+  end.
+
+%% Returns the type and record definitions in a kmodule.
+%% Records are replaced by equivalent types.
+extract_type_definitions(Kmodule) ->
+  %% Replaces the record references in the type forms.
+  TypeForms = cuter_cerl:kmodule_type_forms(Kmodule),
+  Types = [replace_record_references_in_type_form(TF) || TF <- TypeForms],
+  %% Generate equivalent type for the records.
+  RecordForms = cuter_cerl:kmodule_record_forms(Kmodule),
+  Records = [generate_type_form_for_record_form(RF) || RF <- RecordForms],
+  Types ++ Records.
+
+%% Replaces all record references with their respective temporary type
+%% in a type form.
+replace_record_references_in_type_form({Line, {Name, Type, Args}}) ->
+  {Line, {Name, replace_record_references(Type), Args}}.
+
+%% Replaces all the record within specs, with the respective generated types.
+replace_records_in_spec(Spec) ->
+  replace_records_in_spec(Spec, []).
+
+replace_records_in_spec([], FClauses) ->
+  lists:reverse(FClauses);
+replace_records_in_spec([{type, _, _, Ts}=FC|FCs], FClauses) ->
+  NTs = [replace_record_references(T) || T <- Ts],
+  replace_records_in_spec(FCs, [setelement(4, FC, NTs)|FClauses]).
+
+%% Replaces all record references with their respective temporary type.
+replace_record_references({type, L, record, [{atom, _, Name}]}) ->
+  {user_type, L, type_name_for_record(Name), []};
+replace_record_references({T, L, Type, Args}) when T =:= type orelse T =:= user_type ->
+  case is_list(Args) of
+    true ->
+      {T, L, Type, [replace_record_references(A) || A <- Args]};
+    false ->
+      {T, L, Type, Args}
+  end;
+replace_record_references(F) -> F.
+
+%% Generates a type definition for a record.
+%% A record is represented as a tuple where the first element is the name of
+%% the record.  The remaining elements are the types of the record fields.
+generate_type_form_for_record_form({Line, {Name, Fields}}) ->
+  Fs = [replace_record_references(T) || {typed_record_field, _, T} <- Fields],
+  RecType = {type, Line, tuple, [{atom, Line, Name} | Fs]},
+  {Line, {type_name_for_record(Name), RecType, []}}.
+
+%% Returns the name of a generated type that represents the record RecordName.
+type_name_for_record(RecordName) ->
+  list_to_atom(?CUTER_RECORD_TYPE_PREFIX ++ atom_to_list(RecordName)).
+
+%% Transforms the spec and replaces all the clauses that are expressed
+%% as bounded functions, to their equivalent unbounded ones.
+transform_bounded_funs_in_spec(Spec) ->
+  [transform_bounded_fun(C) || C <- Spec].
+
+transform_bounded_fun({type, _L, 'fun', _Sig} = FC) -> FC;
+transform_bounded_fun({type, _L, 'bounded_fun', [Func, Constraints]} = FC) ->
+  Ms = dict:from_list([extract_var_type_from_constraint(C) || C <- Constraints]),
+  case simplify_var_mappings(Ms) of
+    error -> FC;
+    {ok, NMs} -> generate_nonbounded_fun(Func, NMs)
+  end.
+
+extract_var_type_from_constraint({type, _, constraint, [{atom, _, is_subtype}, [{var, _, V}, T]]}) ->
+  {V, T}.
+
+%% Simplifies the types of constraint variables.
+%% The input is a dictionary of variables mapped to their types.
+%% Note that it supports only non-recursive declarations.
+simplify_var_mappings(Ms) ->
+  %% If there are no recursive variables, the computation will end in
+  %% steps at most equal to the number of variables.
+  simplify_var_mappings_pass(Ms, dict:size(Ms), 0).
+
+simplify_var_mappings_pass(_Ms, Lim, N) when N > Lim -> error;
+simplify_var_mappings_pass(Ms, Lim, N) ->
+  Vars = dict:fetch_keys(Ms),
+  Fn = fun(Key, D) ->
+	   T = dict:fetch(Key, D),
+	   case substitute_vars_in_type(T, Ms) of
+	     T -> D;
+	     NewT -> dict:store(Key, NewT, D)
+	   end
+   end,
+  NMs = lists:foldl(Fn, Ms, Vars),
+  case are_dicts_equal_on_keys(Vars, Ms, NMs) of
+    true -> {ok, NMs};
+    false -> simplify_var_mappings_pass(NMs, Lim, N + 1)
+  end.
+
+%% Replace variables in a bounded fun with their produced type forms.
+substitute_vars_in_type({type, _, record, _R} = T, _Ms) -> T;
+substitute_vars_in_type({_, _, _, Args}=T, Ms) when is_list(Args) ->
+  NewArgs = [substitute_vars_in_type(A, Ms) || A <- Args],
+  setelement(4, T, NewArgs);
+substitute_vars_in_type({var, L, Var}, Ms) ->
+  case dict:find(Var, Ms) of
+    error -> form_any(L);
+    {ok, T} -> T
+  end;
+substitute_vars_in_type({ann_type, _, [_Var, T]}, Ms) ->
+  substitute_vars_in_type(T, Ms);
+substitute_vars_in_type(T, _Ms) -> T.
+
+form_any(L) ->
+  {type, L, any, []}.
+
+are_dicts_equal_on_keys([], _D1, _D2) -> true;
+are_dicts_equal_on_keys([K|Ks], D1, D2) ->
+  dict:fetch(K, D1) =:= dict:fetch(K, D2) andalso are_dicts_equal_on_keys(Ks, D1, D2).
+
+%% Generates a non-bounded fun from a bounded fun given the type substitutions
+%% for constraints on the variables.
+generate_nonbounded_fun({type, L, 'fun', [Args, Range]}, Ms) ->
+  NewArgs = substitute_vars_in_type(Args, Ms),
+  NewRange = substitute_vars_in_type(Range, Ms),
+  {type, L, 'fun', [NewArgs, NewRange]}.
+
+warn_unhandled_spec(MFA) ->
+  Slogan = "\033[00;33mWarning: Cannot convert spec of ~s~n\033[00m",
+  io:format(standard_error, Slogan, [mfa_to_string(MFA)]).
+
+%% ============================================================================
+%% Utilities
+%% ============================================================================
+
+%% Returns the string representation of an MFA.
+-spec mfa_to_string(mfa()) -> string().
+mfa_to_string({M, F, A}) ->
+  atom_to_list(M) ++ ":" ++ atom_to_list(F) ++ "/" ++ integer_to_list(A).
+
+-spec are_sets_equal(sets:set(), sets:set()) -> boolean().
+are_sets_equal(A, B) ->
+  %% A = B, iff A ⊆ B and B ⊆ A.
+  sets:is_subset(A, B) andalso sets:is_subset(B, A).
diff --git a/test/ftest/src/reduce_search_space.erl b/test/ftest/src/reduce_search_space.erl
index 3f82d55f..cb3c264c 100644
--- a/test/ftest/src/reduce_search_space.erl
+++ b/test/ftest/src/reduce_search_space.erl
@@ -1,5 +1,5 @@
 -module(reduce_search_space).
--export([f/1]).
+-export([f/1, f6/1, f7/2, f9/1]).
 
 %% Functions that showcase situations where we can prune
 %% the search space of executions.
@@ -23,3 +23,92 @@ h(6) -> 1;
 h(1) -> 7;
 h(3) -> 5;
 h(_) -> 23.
+
+
+%% Tests f1-f6 compose a graph if f6 is called. Testing f6 tests the integrity
+%% of the callgraph calculation and transformation
+
+f1(X) -> % error-free
+  case X of
+    3 ->
+      f2(2);
+    2 ->
+      f2(1);
+    _ -> 1
+  end.
+
+f2(X) -> % error-free
+  case X of
+    3 ->
+      f1(2);
+    2 ->
+      f1(1);
+    _ -> 1
+  end.
+
+f3(X) -> % possibly-erroneous
+  case X of
+    3 ->
+      f4(2);
+    2 ->
+      f4(1);
+    1 -> 1
+  end.
+
+f4(X) -> % possibly-erroneous
+  case X of
+    3 ->
+      f4(2);
+    2 ->
+      f3(1);
+    1 -> 1
+  end.
+
+f5(X) -> % possibly-erroneous
+  case f1(X) of
+    1 ->
+      f3(X);
+    _ -> 1
+  end.
+
+f6(X) ->
+  case f5(X) of
+    1 ->
+      g(X);
+    _ -> 1
+  end.
+
+f7(X, Y) -> % possibly-erroneous
+  case f8(X) of % this call to f8 should not be pruned
+    1 -> f8(Y); % this one should
+    _ -> error("error")
+  end.
+
+f8(X) -> % error-free
+  case X of
+    1 -> 1;
+    2 -> 2;
+    _ -> 1
+  end.
+
+-spec f9(integer()) -> boolean().
+f9(X) -> % error free
+  f9(X, []).
+
+-spec f9(integer(), [integer()]) -> boolean().
+f9(X, Found) ->
+  case X of
+    1 -> true;
+    _ ->
+      case lists:member(X, Found) of
+	false ->
+	  case X rem 2 of
+	    0 ->
+	      f9(X div 2, [X|Found]);
+	    _ ->
+	      f9(3 * X + 1, [X|Found])
+	  end;
+	true ->
+	  false
+      end
+  end.
diff --git a/test/ftests.json b/test/ftests.json
index aeca4bda..748b4eac 100644
--- a/test/ftests.json
+++ b/test/ftests.json
@@ -1243,14 +1243,52 @@
             "depth": "25",
             "errors": true,
             "arity": 1,
+	    "opts": "-ps --disable-pmatch",
             "solutions": [
                 "[3]"
             ],
             "solver": {
-              "SAT": 3,
-              "UNSAT": 6
+              "SAT": 3
             },
             "skip": false
+        },
+	{
+            "module": "reduce_search_space",
+            "function": "f6",
+            "args": "[0]",
+            "depth": "25",
+            "errors": true,
+	    "nondeterministic": true,
+            "arity": 1,
+	    "opts": "-ps --disable-pmatch",
+            "solutions": [
+                "$1 != 1 and $1 != 2 and $1 != 3"
+            ],
+            "skip": false
+        },
+	{
+            "module": "reduce_search_space",
+            "function": "f7",
+            "args": "[0, 0]",
+            "depth": "25",
+            "errors": true,
+	    "nondeterministic": true,
+            "arity": 2,
+	    "opts": "-ps --disable-pmatch",
+            "solutions": [
+                "$1 == 2"
+            ],
+            "skip": false
+        },
+	{
+            "module": "reduce_search_space",
+            "function": "f9",
+            "args": "[10]",
+            "depth": "25",
+            "errors": false,
+            "arity": 1,
+	    "opts": "-ps --disable-pmatch",
+            "skip": false
         }
     ]
 }
diff --git a/test/utest/src/callgraph_examples.erl b/test/utest/src/callgraph_examples.erl
new file mode 100644
index 00000000..01f29c60
--- /dev/null
+++ b/test/utest/src/callgraph_examples.erl
@@ -0,0 +1,60 @@
+-module(callgraph_examples).
+-export([f1/1, f2/1, f3/1, f4/1]).
+
+-spec f1(integer()) -> integer().
+f1(X) ->
+  f11(X).
+
+f11(_X) -> ok.
+
+%% =====================================
+
+-spec f2(integer()) -> integer().
+f2(X) ->
+  case X of
+    1 -> 1;
+    _ -> f21(X - 1)
+  end.
+
+f21(X) ->
+  case X of
+    2 -> 2;
+    _ -> f2(X)
+  end.
+
+%% =====================================
+
+-spec f3([any()]) -> any().
+f3(X) ->
+  [f31(Y) || Y <- X].
+
+f31(X) ->
+  Y = f32(X-1),
+  Y + 1.
+
+f32(X) ->
+  case X of
+    1 -> 1 + f33(4);
+    _ -> f31(X - 1)
+  end.
+
+f33(X) ->
+  X + 1.
+
+%% =====================================
+
+-spec f4(any()) -> any().
+f4(X) ->
+  F = fun(Y) -> f41(Y) end,
+  F(X).
+
+f41(X) ->
+  f42(X + 1).
+
+f42(X) ->
+  f4(X + 1) + f43(X).
+
+f43(X) ->
+  f41(X + 1) + f44(X).
+
+f44(X) -> X.
diff --git a/test/utest/src/cuter_cerl_tests.erl b/test/utest/src/cuter_cerl_tests.erl
index 8ebcd600..e346e7e1 100644
--- a/test/utest/src/cuter_cerl_tests.erl
+++ b/test/utest/src/cuter_cerl_tests.erl
@@ -20,13 +20,10 @@ exported_mfas_in_lists_module_test_() ->
   TagGen = fun() -> {?BRANCH_TAG_PREFIX, 42} end,
   {ok, Klists} = cuter_cerl:load(lists, TagGen, false),
   MfaKfuns = kfuns_from_exports(lists, Klists),
-  Assertions = [{mfa_to_string(Mfa), assert_is_exported(Kfun)} || {Mfa, Kfun} <- MfaKfuns],
+  Assertions = [{cuter_types:mfa_to_string(Mfa), assert_is_exported(Kfun)} || {Mfa, Kfun} <- MfaKfuns],
   R = cuter_cerl:destroy_kmodule(Klists),
   Assertions ++ [?_assertEqual(ok, R)].
 
-mfa_to_string({M, F, A}) ->
-  atom_to_list(M) ++ ":" ++ atom_to_list(F) ++ "/" ++ integer_to_list(A).
-
 kfuns_from_exports(M, Kmodule) ->
   Mfas = [{M, F, A} || {F, A} <- M:module_info(exports)],
   Fn = fun(Mfa) ->
diff --git a/test/utest/src/cuter_graphs_tests.erl b/test/utest/src/cuter_graphs_tests.erl
new file mode 100644
index 00000000..a2e0ebc4
--- /dev/null
+++ b/test/utest/src/cuter_graphs_tests.erl
@@ -0,0 +1,128 @@
+%% -*- erlang-indent-level: 2 -*-
+%%------------------------------------------------------------------------------
+-module(cuter_graphs_tests).
+
+-include_lib("eunit/include/eunit.hrl").
+%-include("include/eunit_config.hrl").
+%-include("include/cuter_macros.hrl").
+
+-spec test() -> ok | {error, any()}.
+
+-spec calculate_dag_callgraph_test_() -> [{string(), {'setup', fun(), fun(), fun()}}].
+calculate_dag_callgraph_test_() ->
+  EntryPoints = [
+		 {callgraph_examples, f1, 1},
+		 {callgraph_examples, f2, 1},
+		 {callgraph_examples, f3, 1},
+		 {callgraph_examples, f4, 1}
+		],
+  Setup = fun(E) -> fun() -> setup(E) end end,
+  Inst = fun validate_callgraph/1,
+  Cleanup = fun cleanup/1,
+  [{"Calculate callgraphs", {setup, Setup(E), Cleanup, Inst}} || E <- EntryPoints].
+
+setup(EntryPoint) ->
+  {G, _, NewEntryPoint} = cuter_graphs:calculate_dag_callgraph(EntryPoint),
+  {EntryPoint, NewEntryPoint, G}.
+
+validate_callgraph({EntryPoint, NewEntryPoint, G}) ->
+  E = fun(F, A) -> {callgraph_examples, F, A} end,
+  N = fun(X) -> {node, X} end,
+  C = fun(X) -> {cycle, X} end,
+  case EntryPoint of
+    {callgraph_examples, f1, 1} ->
+      Nodes = [N(E(f1, 1)), N(E(f11, 1))],
+      Children = [[N(E(f11, 1))], []],
+      NewEntryPoint1 = N(E(f1, 1));
+    {callgraph_examples, f2, 1} ->
+      Nodes = [C([E(f2, 1), E(f21, 1)])],
+      Children = [[]],
+      NewEntryPoint1 = C([E(f2, 1), E(f21, 1)]);
+    {callgraph_examples, f3, 1} ->
+      Nodes = [
+	       N(E(f3, 1)),
+	       C([E(f31, 1), E(f32, 1)]),
+	       N(E(f33, 1))
+	      ],
+      Children = [
+		  [C([E(f31, 1), E(f32, 1)])],
+		  [N(E(f33, 1))],
+		  []
+		 ],
+      NewEntryPoint1 = N(E(f3, 1));
+    {callgraph_examples, f4, 1} ->
+      Nodes = [
+	       C([E(f4, 1), E(f41, 1), E(f42, 1), E(f43, 1)]),
+	       N(E(f44, 1))
+	      ],
+      Children = [
+		  [N(E(f44, 1))],
+		  []
+		 ],
+      NewEntryPoint1 = C([E(f4, 1), E(f41, 1), E(f42, 1), E(f43, 1)])
+  end,
+  G1 = cuter_graphs:make_graph_from_children(Nodes, Children),
+  [?_assertEqual(equal_graphs(G, G1), true), ?_assertEqual(equal_entry_points(NewEntryPoint, NewEntryPoint1), true)].
+
+cleanup(_) -> ok.
+
+equal_graphs(G1, G2) ->
+  G1Keys = dict:fetch_keys(G1),
+  G2Keys = dict:fetch_keys(G2),
+  case equal_keys(G1Keys, G2Keys) of
+    false -> false;
+    C -> 
+      G2New = change_keys(G2, C),
+      equal_graphs_helper(G1, G2New)
+  end.
+
+equal_keys(Keys1, Keys2) ->
+  case length(Keys1) =:= length(Keys2) of
+    true -> equal_keys(Keys1, Keys2, dict:new());
+    false -> false
+  end.
+
+equal_keys([], _, Acc) -> Acc;
+equal_keys([{KeyType, K1}=Key1|Keys1], Keys2, Acc) ->
+  case KeyType of
+    node ->
+      case [K || K <- Keys2, K =:= Key1] of
+	[] -> false;
+	[_] -> equal_keys(Keys1, Keys2, Acc)
+      end;
+    cycle ->
+      case [K2 || {cycle, K2} <- Keys2, cuter_types:are_sets_equal(sets:from_list(K1), sets:from_list(K2))] of
+	[] -> false;
+	[K2] ->
+	  equal_keys(Keys1, Keys2, dict:store(K2, K1, Acc))
+      end
+  end.
+
+change_keys(G, C) ->
+  H = change_keys_helper(dict:to_list(G), C, []),
+  dict:from_list(H).
+  
+change_keys_helper([], _, Acc) -> lists:reverse(Acc);
+change_keys_helper([{{node, _}, _N}=K|Ks], C, Acc)->
+  change_keys_helper(Ks, C, [K|Acc]);
+change_keys_helper([{{cycle, Cycle}, N}|Ks], C, Acc) ->
+  change_keys_helper(Ks, C, [{{cycle, dict:fetch(Cycle, C)}, N}|Acc]).
+
+equal_graphs_helper(G1, G2) ->
+  F = fun(Node, N1, Acc) ->
+	  N2 = dict:fetch(Node, G2),
+	  case equal_keys(N1, N2) of
+	    false -> Acc;
+	    _ -> true
+	  end
+      end,
+  dict:fold(F, false, G1).
+
+equal_entry_points({T, E1}, {T, E2}) ->
+  case T of
+    node -> E1 =:= E2;
+    cycle -> cuter_types:are_sets_equal(sets:from_list(E1), sets:from_list(E2))
+  end;
+equal_entry_points(_, _) -> false.
+
+  
diff --git a/test/utest/src/cuter_types_tests.erl b/test/utest/src/cuter_types_tests.erl
index 54ff7744..f6f2806b 100644
--- a/test/utest/src/cuter_types_tests.erl
+++ b/test/utest/src/cuter_types_tests.erl
@@ -21,54 +21,52 @@ parse_types({types_and_specs, Attrs}) ->
   Ts = [
     {"t1()"
     , {type, t1, 0}
-    , { cuter_types:t_atom()
-       , []
-      }
+    , {cuter_types:t_atom(), []}
     },
     {"t2()"
     , {type, t2, 0}
-    , { cuter_types:t_tuple([cuter_types:t_integer(), cuter_types:t_float(), cuter_types:t_tuple()])
+    , {cuter_types:t_tuple([cuter_types:t_integer(), cuter_types:t_float(), cuter_types:t_tuple()])
       , []
       }
     },
     {"t3()"
     , {type, t3, 0}
-    , { cuter_types:t_union([cuter_types:t_any(), cuter_types:t_nil()])
+    , {cuter_types:t_union([cuter_types:t_any(), cuter_types:t_nil()])
       , []
       }
     },
     {"t4()"
     , {type, t4, 0}
-    , { cuter_types:t_list(cuter_types:t_union([cuter_types:t_list(), cuter_types:t_bitstring()]))
+    , {cuter_types:t_list(cuter_types:t_union([cuter_types:t_list(), cuter_types:t_bitstring()]))
       , []
       }
     },
     {"t5()"
     , {type, t5, 0}
-    , { cuter_types:t_tuple([
-          cuter_types:t_binary(), cuter_types:t_nonempty_list(cuter_types:t_number()),
-          cuter_types:t_string(), cuter_types:t_char()
-        ])
+    , {cuter_types:t_tuple([
+         cuter_types:t_binary(), cuter_types:t_nonempty_list(cuter_types:t_number()),
+         cuter_types:t_string(), cuter_types:t_char()
+       ])
       , []
       }
     },
     {"t7()"
     , {type, t7, 0}
-    , { cuter_types:t_union([
-          cuter_types:t_bitstring(64, 0), cuter_types:t_bitstring(0, 3), cuter_types:t_bitstring(128, 12)
+    , {cuter_types:t_union([
+         cuter_types:t_bitstring(64, 0), cuter_types:t_bitstring(0, 3), cuter_types:t_bitstring(128, 12)
         ])
       , []
       }
     },
     {"t8()"
     , {type, t8, 0}
-    , { cuter_types:t_map(), [] }
+    , {cuter_types:t_map(), []}
     },
     {"t9()"
     , {type, t9, 0}
-    , { cuter_types:t_map([
-        { map_field_assoc, cuter_types:t_atom(), cuter_types:t_list(cuter_types:t_integer()) },
-        { map_field_exact, cuter_types:t_float(), cuter_types:t_float() }
+    , {cuter_types:t_map([
+        {map_field_assoc, cuter_types:t_atom(), cuter_types:t_list(cuter_types:t_integer())},
+        {map_field_exact, cuter_types:t_float(), cuter_types:t_float()}
         ])
       , []
     }
@@ -81,3 +79,85 @@ setup(Mod) ->
   {Mod, Attrs}.
 
 cleanup(_) -> ok.
+
+-spec convert_types_test() -> 'ok'.
+convert_types_test() ->
+  Modules = [examples_for_spec_conversion, examples_for_spec_conversion_pair],
+  Fn = fun(M) -> {ok, AST} = cuter_cerl:get_core(M, false), AST end,
+  Xs = [{M, Fn(M)} || M <- Modules],
+  TagGen = fun() -> ok end,
+  Kmodules = [cuter_cerl:kmodule(M, AST, TagGen) || {M, AST} <- Xs],
+  Specs = cuter_types:specs_as_erl_types(Kmodules),
+  Expect = spec_conversion_tests(),
+  lists:foreach(fun (E) -> spec_assertions(E, Specs) end, Expect),
+  ExpectMfas = lists:sort([Mfa || {Mfa, _Spec} <- Expect]),
+  GotMfas = lists:sort(dict:fetch_keys(Specs)),
+  ?assertEqual(ExpectMfas, GotMfas),
+  ok.
+
+spec_assertions({Mfa, Expect}, R) ->
+  case dict:find(Mfa, R) of
+    error ->
+      Comment = cuter_types:mfa_to_string(Mfa) ++ " should exist",
+      ?assert(dict:is_key(Mfa, R), Comment);
+    {ok, Got} ->
+      Comment = "Spec of " ++ cuter_types:mfa_to_string(Mfa),
+      ?assertEqual(Expect, Got, Comment)
+  end.
+
+spec_conversion_tests() ->
+  T_Animal = erl_types:t_atoms([cat, dog]),
+  T_Point = erl_types:t_tuple([erl_types:t_atom(point), 
+			       erl_types:t_number(), erl_types:t_number()]),
+  [
+    {
+      {examples_for_spec_conversion, id, 1},
+      [erl_types:t_fun([erl_types:t_any()], erl_types:t_any())]
+    },
+    {
+      {examples_for_spec_conversion, inc, 1},
+      [erl_types:t_fun([erl_types:t_integer()], erl_types:t_integer())]
+    },
+    {
+      {examples_for_spec_conversion, to_atom, 1},
+      [erl_types:t_fun(
+	 [erl_types:t_sup(erl_types:t_integer(), erl_types:t_atom())],
+	 erl_types:t_atom())]
+    },
+    {
+      {examples_for_spec_conversion, translate, 3},
+      [erl_types:t_fun(
+        [T_Point, erl_types:t_number(), erl_types:t_number()],
+        T_Point)]
+    },
+    {
+      {examples_for_spec_conversion, root, 1},
+      []  %% FIX: We do not support recursive types.
+    },
+    {
+      {examples_for_spec_conversion, max_x, 1},
+      [erl_types:t_fun([erl_types:t_list(T_Point)], erl_types:t_number())]
+    },
+    {
+      {examples_for_spec_conversion, is_dog, 1},
+      [erl_types:t_fun([T_Animal], erl_types:t_boolean())]
+    },
+    {
+      {examples_for_spec_conversion_pair, to_int, 1},
+      [erl_types:t_fun(
+        [erl_types:t_sup(erl_types:t_integer(), erl_types:t_atom())],
+        erl_types:t_integer())]
+    },
+    {
+      {examples_for_spec_conversion_pair, can_bark, 1},
+      [erl_types:t_fun([erl_types:t_list(T_Animal)], erl_types:t_boolean())]
+    },
+    {
+      {examples_for_spec_conversion_pair, count_trees, 1},
+      []  %% FIX: We do not support mutually recursive declarations in bounded funs.
+    },
+    {
+      {examples_for_spec_conversion_pair, tree_height, 1},
+      []  %% FIX: We do not support recursive declarations in bounded funs.
+    }
+  ].
diff --git a/test/utest/src/examples_for_spec_conversion.erl b/test/utest/src/examples_for_spec_conversion.erl
new file mode 100644
index 00000000..02a2a6f4
--- /dev/null
+++ b/test/utest/src/examples_for_spec_conversion.erl
@@ -0,0 +1,38 @@
+-module(examples_for_spec_conversion).
+
+-export([id/1, inc/1, to_atom/1, translate/3, root/1, max_x/1, is_dog/1]).
+
+-export_type([t_int_or_atom/0]).
+
+-type t_int_or_atom() :: t_int() | atom().
+-type t_int() :: integer().
+
+-record(point, {x :: number(), y :: number()}).
+-type point() :: #point{}.
+
+-type tree() :: {integer(), tree(), tree()} | nil.
+
+-type list_of(X) :: [X].
+
+-spec id(X) -> X when X :: term().
+id(X) -> X.
+
+-spec inc(t_int()) -> t_int().
+inc(X) -> X + 1.
+
+-spec to_atom(t_int_or_atom()) -> atom().
+to_atom(X) when is_atom(X) -> X;
+to_atom(X) when is_integer(X) -> list_to_atom([$0 + X]).
+
+-spec translate(#point{}, number(), number()) -> point().
+translate(#point{x=X, y=Y}, DX, DY) -> #point{x = X + DX, y = Y + DY}.
+
+-spec root(tree()) -> integer() | nil.
+root({X, _L, _R}) -> X;
+root(nil) -> nil.
+
+-spec max_x(list_of(#point{})) -> number().
+max_x(Ps) -> lists:max([P#point.x || P <- Ps]).
+
+-spec is_dog(examples_for_spec_conversion_pair:t_animal()) -> boolean().
+is_dog(X) -> X =:= dog.
diff --git a/test/utest/src/examples_for_spec_conversion_pair.erl b/test/utest/src/examples_for_spec_conversion_pair.erl
new file mode 100644
index 00000000..80e22037
--- /dev/null
+++ b/test/utest/src/examples_for_spec_conversion_pair.erl
@@ -0,0 +1,40 @@
+-module(examples_for_spec_conversion_pair).
+
+-export([to_int/1, can_bark/1, count_trees/1, tree_height/1]).
+
+-export_type([t_animal/0]).
+
+-type t_animal() :: dog | cat.
+
+-spec to_int(examples_for_spec_conversion:t_int_or_atom()) -> integer().
+to_int(X) when is_integer(X) -> X;
+to_int(X) when is_atom(X) -> lists:max(atom_to_list(X)).
+
+-spec can_bark(Animals) -> boolean() when
+        Animals :: [Animal],
+        Animal :: t_animal().
+can_bark(Animals) -> lists:any(fun (A) -> A =:= dog end, Animals).
+
+-spec count_trees(Forest) -> integer() when
+        Forest :: {Tree, Forest} | nil,
+        Tree :: {atom(), Forest} | empty.
+count_trees(F) ->
+  count_trees([F], 0).
+
+count_trees([], N) -> N;
+count_trees([nil|Forests], N) ->
+  count_trees(Forests, N);
+count_trees([{empty, Forest}|Forests], N) ->
+  count_trees([Forest|Forests], N + 1);
+count_trees([{{_Name, InnerForest}, Forest}|Forests], N) ->
+  count_trees([InnerForest, Forest|Forests], N + 1).
+
+-spec tree_height(Tree) -> integer() when
+        Tree :: Node | Leaf,
+        Node :: {Tree, Tree},
+        Leaf :: nil.
+tree_height(nil) -> 0;
+tree_height({Left, Right}) ->
+  H1 = tree_height(Left),
+  H2 = tree_height(Right),
+  1 + max(H1, H2).