diff --git a/src/concrete/semantics.mlw b/src/concrete/semantics.mlw
index df5505d0..d641a898 100644
--- a/src/concrete/semantics.mlw
+++ b/src/concrete/semantics.mlw
@@ -77,6 +77,9 @@ module Buffers
 
   val function split_on_default_ifs string : list string 
 
+  let constant loop_limit_message = "[INCOMPLETE] Loop limit"
+  let constant stack_limit_message = "[INCOMPLETE] Stack limit"
+
   scope Stdout
 
     use bool.Bool
@@ -106,10 +109,10 @@ module Buffers
     let function to_stdin out =
       reverse (all_lines out)
 
-    let output str out =
+    let function output str out =
       { out with line = String.concat out.line str }
 
-    let newline out =
+    let function newline out =
       { line = ""; lines = Cons out.line out.lines }
 
     (* http://pubs.opengroup.org/onlinepubs/9699919799/utilities/V3_chap02.html#tag_18_06_03 *)
@@ -653,7 +656,8 @@ module Semantics
     eval_list_expr stk (inp, ctx, sta) es (sta1, Ok args) ->
     ctx.func_env[id] = Some ins ->
     inp.config.stack_size = Finite stk ->
-    eval_instruction stk (inp, ctx, sta) (ICallFunction id es) (sta1, ctx, BIncomplete)
+    let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in
+    eval_instruction stk (inp, ctx, sta) (ICallFunction id es) (sta1', ctx, BIncomplete)
 
   | eval_call_function: forall stk inp ctx ctx2 sta sta1 sta2 id es args ins bhv.
     eval_list_expr stk (inp, ctx, sta) es (sta1, Ok args) ->
@@ -704,7 +708,8 @@ module Semantics
   | eval_while_loop_limit: forall stk ctr b inp ctx sta ins1 ins2.
     0 <= ctr ->
     inp.config.loop_limit = Finite ctr ->
-    eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta, ctx, BIncomplete) ctr b
+    let sta' = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in
+    eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta', ctx, BIncomplete) ctr b
 
   (** Condition not normal *)
   | eval_while_abort_condition: forall stk ctr b inp ctx ctx1 sta sta1 ins1 ins2 bhv1.
diff --git a/src/symbolic/symbolicInterpreter.mlw b/src/symbolic/symbolicInterpreter.mlw
index 45517887..9c6f5082 100644
--- a/src/symbolic/symbolicInterpreter.mlw
+++ b/src/symbolic/symbolicInterpreter.mlw
@@ -686,7 +686,7 @@ module Interpreter
             if stk = get_finite inp.config.stack_size then (* Stack overflow *)
               let aux arg =
                 let sta', _ = arg in
-                (* let sta' = { sta' with log = Stdout.(newline (output "INCOMPLETE: STACK_OVERFLOW" sta'.log)) } in *)
+                let sta' = { sta' with log = Stdout.(newline (output stack_limit_message sta'.log)) } in
                 {state=sta'; context=ctx; data=()}
               in
               Rs.({empty with failure = Cn.map aux arg_res})
@@ -695,7 +695,8 @@ module Interpreter
                 eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
                 ctx.func_env[id] = Some ins ->
                 inp.config.stack_size = Finite stk ->
-                Rs.mem {state=sta1; context=ctx; data=()} BIncomplete result
+                let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in
+                Rs.mem {state=sta1'; context=ctx; data=()} BIncomplete result
               }
             else (* Execute function *)
               let res2 =
@@ -1003,7 +1004,7 @@ module Interpreter
     }
   = let loop_limit = get_finite inp.config.loop_limit in
     if ctr = loop_limit then
-      (* let sta = { sta with log = Stdout.(newline (output "INCOMPLETE: LOOP_LIMIT" sta.log)) } in *)
+      let sta = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in
       Rs.({empty with failure=Cn.singleton {state=sta; context=ctx; data=(ctr, b)}})
     else
       let res1_normal, res1_abort =