diff --git a/CHANGES.md b/CHANGES.md
index 80e82fd0..ef7d25d8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,8 @@
 # Unreleased
 
 - Improve test-failure message
-  [\#202](https://github.com/ocaml-gospel/ortac/pull/202)
+  [\#202](https://github.com/ocaml-gospel/ortac/pull/202) and
+  [\#204](https://github.com/ocaml-gospel/ortac/pull/204)
 - Add a comment warning that the file is generated
   [\#198](https://github.com/ocaml-gospel/ortac/pull/198)
 - Add support for type invariants
diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml
index 89e70aeb..9a44bdc7 100644
--- a/examples/lwt_dllist_tests.ml
+++ b/examples/lwt_dllist_tests.ml
@@ -19,16 +19,16 @@ module Spec =
       | Take_opt_r 
     let show_cmd cmd__001_ =
       match cmd__001_ with
-      | Is_empty -> Format.asprintf "%s" "is_empty"
-      | Length -> Format.asprintf "%s" "length"
+      | Is_empty -> Format.asprintf "%s sut" "is_empty"
+      | Length -> Format.asprintf "%s sut" "length"
       | Add_l a_1 ->
-          Format.asprintf "%s %a" "add_l" (Util.Pp.pp_int true) a_1
+          Format.asprintf "%s %a sut" "add_l" (Util.Pp.pp_int true) a_1
       | Add_r a_2 ->
-          Format.asprintf "%s %a" "add_r" (Util.Pp.pp_int true) a_2
-      | Take_l -> Format.asprintf "%s" "take_l"
-      | Take_r -> Format.asprintf "%s" "take_r"
-      | Take_opt_l -> Format.asprintf "%s" "take_opt_l"
-      | Take_opt_r -> Format.asprintf "%s" "take_opt_r"
+          Format.asprintf "%s %a sut" "add_r" (Util.Pp.pp_int true) a_2
+      | Take_l -> Format.asprintf "%s sut" "take_l"
+      | Take_r -> Format.asprintf "%s sut" "take_r"
+      | Take_opt_l -> Format.asprintf "%s sut" "take_opt_l"
+      | Take_opt_r -> Format.asprintf "%s sut" "take_opt_r"
     type nonrec state = {
       contents: int Ortac_runtime.Gospelstdlib.sequence }
     let init_state =
@@ -336,7 +336,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           then None
           else
             Some
-              (Ortac_runtime.report "is_empty"
+              (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
                  [("b <-> s.contents = Sequence.empty",
                     {
                       Ortac_runtime.start =
@@ -384,7 +385,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           then None
           else
             Some
-              (Ortac_runtime.report "length"
+              (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
                  [("l = Sequence.length s.contents",
                     {
                       Ortac_runtime.start =
@@ -441,7 +443,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "take_l"
+                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                      (Some (Res (Ortac_runtime.dummy, ()))) "take_l"
                       [("if old s.contents = Sequence.empty\n              then false\n              else a = Sequence.hd (old s.contents)",
                          {
                            Ortac_runtime.start =
@@ -493,7 +496,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "take_l"
+                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()" None
+                      "take_l"
                       [("old s.contents = Sequence.empty = s.contents",
                          {
                            Ortac_runtime.start =
@@ -553,7 +557,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "take_r"
+                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                      (Some (Res (Ortac_runtime.dummy, ()))) "take_r"
                       [("if old s.contents = Sequence.empty\n              then false\n              else a = (old s.contents)[Sequence.length (old s.contents) - 1]",
                          {
                            Ortac_runtime.start =
@@ -605,7 +610,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "take_r"
+                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()" None
+                      "take_r"
                       [("old s.contents = Sequence.empty = s.contents",
                          {
                            Ortac_runtime.start =
@@ -657,7 +663,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           then None
           else
             Some
-              (Ortac_runtime.report "take_opt_l"
+              (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "take_opt_l"
                  [("old s.contents = match o with\n                                | None -> Sequence.empty\n                                | Some a -> Sequence.cons a s.contents",
                     {
                       Ortac_runtime.start =
@@ -708,7 +715,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           then None
           else
             Some
-              (Ortac_runtime.report "take_opt_r"
+              (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "take_opt_r"
                  [("old s.contents = match o with\n                                | None -> Sequence.empty\n                                | Some a -> Sequence.snoc s.contents a",
                     {
                       Ortac_runtime.start =
diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml
index 3ca9f4ff..a9316d35 100644
--- a/examples/varray_circular_tests.ml
+++ b/examples/varray_circular_tests.ml
@@ -80,28 +80,29 @@ module Spec =
     let show_cmd cmd__003_ =
       match cmd__003_ with
       | Push_back x ->
-          Format.asprintf "%s %a" "push_back"
+          Format.asprintf "%s sut %a" "push_back"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x
-      | Pop_back -> Format.asprintf "%s" "pop_back"
+      | Pop_back -> Format.asprintf "%s sut" "pop_back"
       | Push_front x_1 ->
-          Format.asprintf "%s %a" "push_front"
+          Format.asprintf "%s sut %a" "push_front"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x_1
-      | Pop_front -> Format.asprintf "%s" "pop_front"
+      | Pop_front -> Format.asprintf "%s sut" "pop_front"
       | Insert_at (i_1, x_2) ->
-          Format.asprintf "%s %a %a" "insert_at" (Util.Pp.pp_int true) i_1
-            (Util.Pp.pp_elt Util.Pp.pp_char true) x_2
+          Format.asprintf "%s sut %a %a" "insert_at" (Util.Pp.pp_int true)
+            i_1 (Util.Pp.pp_elt Util.Pp.pp_char true) x_2
       | Pop_at i_2 ->
-          Format.asprintf "%s %a" "pop_at" (Util.Pp.pp_int true) i_2
+          Format.asprintf "%s sut %a" "pop_at" (Util.Pp.pp_int true) i_2
       | Delete_at i_3 ->
-          Format.asprintf "%s %a" "delete_at" (Util.Pp.pp_int true) i_3
-      | Get i_4 -> Format.asprintf "%s %a" "get" (Util.Pp.pp_int true) i_4
+          Format.asprintf "%s sut %a" "delete_at" (Util.Pp.pp_int true) i_3
+      | Get i_4 ->
+          Format.asprintf "%s sut %a" "get" (Util.Pp.pp_int true) i_4
       | Set (i_5, v) ->
-          Format.asprintf "%s %a %a" "set" (Util.Pp.pp_int true) i_5
+          Format.asprintf "%s sut %a %a" "set" (Util.Pp.pp_int true) i_5
             (Util.Pp.pp_elt Util.Pp.pp_char true) v
-      | Length -> Format.asprintf "%s" "length"
-      | Is_empty -> Format.asprintf "%s" "is_empty"
+      | Length -> Format.asprintf "%s sut" "length"
+      | Is_empty -> Format.asprintf "%s sut" "is_empty"
       | Fill (pos, len, x_3) ->
-          Format.asprintf "%s %a %a %a" "fill" (Util.Pp.pp_int true) pos
+          Format.asprintf "%s sut %a %a %a" "fill" (Util.Pp.pp_int true) pos
             (Util.Pp.pp_int true) len (Util.Pp.pp_elt Util.Pp.pp_char true)
             x_3
     type nonrec state = {
@@ -757,7 +758,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_back"
+                   (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
+                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_back"
                       [("if old t.contents = Sequence.empty\n              then false\n              else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]",
                          {
                            Ortac_runtime.start =
@@ -809,7 +811,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_back"
+                   (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
+                      None "pop_back"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -866,7 +869,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_front"
+                   (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
+                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_front"
                       [("if old t.contents = Sequence.empty\n              then false\n              else proj x = Sequence.hd (old t.contents)",
                          {
                            Ortac_runtime.start =
@@ -918,7 +922,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_front"
+                   (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
+                      None "pop_front"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -974,7 +979,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "insert_at"
+                     (Ortac_runtime.report "Varray_circular_spec"
+                        "make 42 'a'" None "insert_at"
                         [("0 <= i <= Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1036,7 +1042,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "insert_at"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'" None "insert_at"
                            [("0 <= i <= Sequence.length t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1084,7 +1091,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "pop_at"
+                     (Ortac_runtime.report "Varray_circular_spec"
+                        "make 42 'a'" None "pop_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1138,7 +1146,9 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "pop_at"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'"
+                           (Some (Res (Ortac_runtime.dummy, ()))) "pop_at"
                            [("(proj x) = old t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1193,7 +1203,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "pop_at"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'" None "pop_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1241,7 +1252,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "delete_at"
+                     (Ortac_runtime.report "Varray_circular_spec"
+                        "make 42 'a'" None "delete_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1298,7 +1310,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "delete_at"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'" (Some (Res (unit, ()))) "delete_at"
                            [("Sequence.length t.contents = Sequence.length (old t.contents) - 1",
                               {
                                 Ortac_runtime.start =
@@ -1353,7 +1366,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "delete_at"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'" None "delete_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1401,7 +1415,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "get"
+                     (Ortac_runtime.report "Varray_circular_spec"
+                        "make 42 'a'" None "get"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1455,7 +1470,9 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "get"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'"
+                           (Some (Res (Ortac_runtime.dummy, ()))) "get"
                            [("(proj x) = t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1510,7 +1527,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "get"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'" None "get"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1558,7 +1576,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "set"
+                     (Ortac_runtime.report "Varray_circular_spec"
+                        "make 42 'a'" None "set"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1614,7 +1633,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "set"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'" None "set"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1662,7 +1682,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           then None
           else
             Some
-              (Ortac_runtime.report "length"
+              (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
                  [("l = Sequence.length t.contents",
                     {
                       Ortac_runtime.start =
@@ -1710,7 +1731,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           then None
           else
             Some
-              (Ortac_runtime.report "is_empty"
+              (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
                  [("b <-> t.contents = Sequence.empty",
                     {
                       Ortac_runtime.start =
@@ -1773,7 +1795,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "fill"
+                     (Ortac_runtime.report "Varray_circular_spec"
+                        "make 42 'a'" None "fill"
                         [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1845,7 +1868,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "fill"
+                        (Ortac_runtime.report "Varray_circular_spec"
+                           "make 42 'a'" None "fill"
                            [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
                               {
                                 Ortac_runtime.start =
diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml
index 8154cd67..700ebbe0 100644
--- a/examples/varray_tests.ml
+++ b/examples/varray_tests.ml
@@ -80,28 +80,29 @@ module Spec =
     let show_cmd cmd__003_ =
       match cmd__003_ with
       | Push_back x ->
-          Format.asprintf "%s %a" "push_back"
+          Format.asprintf "%s sut %a" "push_back"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x
-      | Pop_back -> Format.asprintf "%s" "pop_back"
+      | Pop_back -> Format.asprintf "%s sut" "pop_back"
       | Push_front x_1 ->
-          Format.asprintf "%s %a" "push_front"
+          Format.asprintf "%s sut %a" "push_front"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x_1
-      | Pop_front -> Format.asprintf "%s" "pop_front"
+      | Pop_front -> Format.asprintf "%s sut" "pop_front"
       | Insert_at (i_1, x_2) ->
-          Format.asprintf "%s %a %a" "insert_at" (Util.Pp.pp_int true) i_1
-            (Util.Pp.pp_elt Util.Pp.pp_char true) x_2
+          Format.asprintf "%s sut %a %a" "insert_at" (Util.Pp.pp_int true)
+            i_1 (Util.Pp.pp_elt Util.Pp.pp_char true) x_2
       | Pop_at i_2 ->
-          Format.asprintf "%s %a" "pop_at" (Util.Pp.pp_int true) i_2
+          Format.asprintf "%s sut %a" "pop_at" (Util.Pp.pp_int true) i_2
       | Delete_at i_3 ->
-          Format.asprintf "%s %a" "delete_at" (Util.Pp.pp_int true) i_3
-      | Get i_4 -> Format.asprintf "%s %a" "get" (Util.Pp.pp_int true) i_4
+          Format.asprintf "%s sut %a" "delete_at" (Util.Pp.pp_int true) i_3
+      | Get i_4 ->
+          Format.asprintf "%s sut %a" "get" (Util.Pp.pp_int true) i_4
       | Set (i_5, v) ->
-          Format.asprintf "%s %a %a" "set" (Util.Pp.pp_int true) i_5
+          Format.asprintf "%s sut %a %a" "set" (Util.Pp.pp_int true) i_5
             (Util.Pp.pp_elt Util.Pp.pp_char true) v
-      | Length -> Format.asprintf "%s" "length"
-      | Is_empty -> Format.asprintf "%s" "is_empty"
+      | Length -> Format.asprintf "%s sut" "length"
+      | Is_empty -> Format.asprintf "%s sut" "is_empty"
       | Fill (pos, len, x_3) ->
-          Format.asprintf "%s %a %a %a" "fill" (Util.Pp.pp_int true) pos
+          Format.asprintf "%s sut %a %a %a" "fill" (Util.Pp.pp_int true) pos
             (Util.Pp.pp_int true) len (Util.Pp.pp_elt Util.Pp.pp_char true)
             x_3
     type nonrec state = {
@@ -757,7 +758,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_back"
+                   (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_back"
                       [("if old t.contents = Sequence.empty\n              then false\n              else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]",
                          {
                            Ortac_runtime.start =
@@ -809,7 +811,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_back"
+                   (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                      "pop_back"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -866,7 +869,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_front"
+                   (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_front"
                       [("if old t.contents = Sequence.empty\n              then false\n              else proj x = Sequence.hd (old t.contents)",
                          {
                            Ortac_runtime.start =
@@ -918,7 +922,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "pop_front"
+                   (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                      "pop_front"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -974,7 +979,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "insert_at"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                        "insert_at"
                         [("0 <= i <= Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1034,7 +1040,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "insert_at"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           None "insert_at"
                            [("0 <= i <= Sequence.length t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1082,7 +1089,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "pop_at"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                        "pop_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1134,7 +1142,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "pop_at"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           (Some (Res (Ortac_runtime.dummy, ()))) "pop_at"
                            [("(proj x) = old t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1187,7 +1196,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "pop_at"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           None "pop_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1235,7 +1245,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "delete_at"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                        "delete_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1290,7 +1301,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "delete_at"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           (Some (Res (unit, ()))) "delete_at"
                            [("Sequence.length t.contents = Sequence.length (old t.contents) - 1",
                               {
                                 Ortac_runtime.start =
@@ -1343,7 +1355,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "delete_at"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           None "delete_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1391,7 +1404,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "get"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                        "get"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1443,7 +1457,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "get"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           (Some (Res (Ortac_runtime.dummy, ()))) "get"
                            [("(proj x) = t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1496,7 +1511,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "get"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           None "get"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1544,7 +1560,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "set"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                        "set"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1598,7 +1615,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "set"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           None "set"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1646,7 +1664,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           then None
           else
             Some
-              (Ortac_runtime.report "length"
+              (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
                  [("l = Sequence.length t.contents",
                     {
                       Ortac_runtime.start =
@@ -1694,7 +1713,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           then None
           else
             Some
-              (Ortac_runtime.report "is_empty"
+              (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
                  [("b <-> t.contents = Sequence.empty",
                     {
                       Ortac_runtime.start =
@@ -1757,7 +1777,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "fill"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
+                        "fill"
                         [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1827,7 +1848,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "fill"
+                        (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                           None "fill"
                            [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
                               {
                                 Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/doc/index.mld b/plugins/qcheck-stm/doc/index.mld
index 435f5df8..0b6e20fd 100644
--- a/plugins/qcheck-stm/doc/index.mld
+++ b/plugins/qcheck-stm/doc/index.mld
@@ -263,6 +263,10 @@ val type_not_supported : new_type -> 'a t -> new_type
 
 {@sh[
 $ ortac qcheck-stm example_unknown_type.mli "make 42 'a'" "char t" -o foo.ml
+File "example_unknown_type.mli", line 15, characters 0-87:
+15 | val type_not_supported : new_type -> 'a t -> new_type
+16 | (*@ y = type_not_supported x t *)
+Warning: Incomplete computation of the returned value in the specification of type_not_supported. Failure message won't be able to display the expected returned value.
 $ grep -A 1 "type cmd" foo.ml
     type cmd =
       | Type_not_supported of new_type
@@ -348,6 +352,11 @@ the command will generate the following warning:
 
 {@sh[
 $ ortac qcheck-stm example_ill_formed_quantification.mli "make 42 'a'" "char t" -o foo.ml
+File "example_ill_formed_quantification.mli", line 13, characters 0-142:
+13 | val unsupported_quantification : 'a t -> bool
+14 | (*@ b = unsupported_quantification t
+15 |     ensures b = forall a. List.mem a t.contents -> a = a *)
+Warning: Incomplete computation of the returned value in the specification of unsupported_quantification. Failure message won't be able to display the expected returned value.
 File "example_ill_formed_quantification.mli", line 15, characters 16-56:
 15 |     ensures b = forall a. List.mem a t.contents -> a = a *)
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -422,6 +431,10 @@ File "example_limitations.mli", line 28, characters 15-25:
 28 | val for_all : ('a -> bool) -> 'a t -> bool
                     ^^^^^^^^^^
 Warning: Skipping for_all: functions are not supported yet as arguments.
+File "example_limitations.mli", line 22, characters 0-50:
+22 | val g : int * int -> 'a t -> bool
+23 | (*@ b = g x t *)
+Warning: Incomplete computation of the returned value in the specification of g. Failure message won't be able to display the expected returned value.
 File "example_limitations.mli", line 22, characters 8-17:
 22 | val g : int * int -> 'a t -> bool
              ^^^^^^^^^
diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index ac6fd680..58e59f97 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -6,6 +6,7 @@ type t = {
   context : Context.t;
   sut_core_type : Ppxlib.core_type;
   init_sut : Ppxlib.expression;
+  init_sut_txt : string;
 }
 
 let get_sut_type_name config =
@@ -74,7 +75,7 @@ let init_sut_from_string str =
   try Parse.expression (Lexing.from_string str) |> Reserr.ok
   with _ -> Reserr.(error (Syntax_error_in_init_sut str, Location.none))
 
-let init path init_sut sut_str =
+let init path init_sut_txt sut_str =
   let open Reserr in
   try
     let module_name = Utils.module_name_of_path path in
@@ -96,7 +97,7 @@ let init path init_sut sut_str =
     in
     let context = List.fold_left add context sigs in
     let* sut_core_type = sut_core_type sut_str
-    and* init_sut = init_sut_from_string init_sut in
-    ok (sigs, { context; sut_core_type; init_sut })
+    and* init_sut = init_sut_from_string init_sut_txt in
+    ok (sigs, { context; sut_core_type; init_sut; init_sut_txt })
   with Gospel.Warnings.Error (l, k) ->
     error (Ortac_core.Warnings.GospelError k, l)
diff --git a/plugins/qcheck-stm/src/ir.ml b/plugins/qcheck-stm/src/ir.ml
index 92a956bf..0e54918f 100644
--- a/plugins/qcheck-stm/src/ir.ml
+++ b/plugins/qcheck-stm/src/ir.ml
@@ -45,6 +45,7 @@ type value = {
   args : (Ppxlib.core_type * Ident.t option) list;
       (* arguments of unit types can be nameless *)
   ret : Ident.t list;
+  ret_values : term list list;
   next_state : next_state;
   precond : Tterm.term list;
   postcond : postcond;
@@ -63,8 +64,19 @@ let get_return_type value =
   in
   aux value.ty
 
-let value id ty inst sut_var args ret next_state precond postcond =
-  { id; ty; inst; sut_var; args; ret; next_state; precond; postcond }
+let value id ty inst sut_var args ret ret_values next_state precond postcond =
+  {
+    id;
+    ty;
+    inst;
+    sut_var;
+    args;
+    ret;
+    ret_values;
+    next_state;
+    precond;
+    postcond;
+  }
 
 type t = {
   state : (Ident.t * Ppxlib.core_type) list;
diff --git a/plugins/qcheck-stm/src/ir_of_gospel.ml b/plugins/qcheck-stm/src/ir_of_gospel.ml
index 1d6a2acf..d4bd60b7 100644
--- a/plugins/qcheck-stm/src/ir_of_gospel.ml
+++ b/plugins/qcheck-stm/src/ir_of_gospel.ml
@@ -167,6 +167,25 @@ let next_state sut state spec =
   in
   ok Ir.{ formulae; modifies }
 
+(* returns the list of terms [t] such that [ret = t] appears in the [ensures] of
+   the [spec] *)
+let returned_value_description spec ret =
+  let open Tterm in
+  let is_ret vs =
+    let open Symbols in
+    Ident.equal ret vs.vs_name
+  in
+  let rec pred t =
+    match t.t_node with
+    (* match [ret = term] and return [term] *)
+    | Tapp (ls, [ { t_node = Tvar vs; _ }; right ])
+      when Symbols.(ls_equal ps_equ ls) && is_ret vs ->
+        [ Ir.term_val spec right ]
+    | Tbinop ((Tand | Tand_asym), l, r) -> pred l @ pred r
+    | _ -> []
+  in
+  List.concat_map pred spec.sp_post
+
 let postcond spec =
   let normal = List.mapi (fun i x -> (i, Ir.term_val spec x)) spec.sp_post
   and exceptional =
@@ -216,10 +235,11 @@ let val_desc config state vd =
     in
     List.map p spec.sp_ret |> sequence
   in
+  let ret_values = List.map (returned_value_description spec) ret in
   let* next_state = next_state sut state spec in
   let postcond = postcond spec in
-  Ir.value vd.vd_name vd.vd_type inst sut args ret next_state spec.sp_pre
-    postcond
+  Ir.value vd.vd_name vd.vd_type inst sut args ret ret_values next_state
+    spec.sp_pre postcond
   |> ok
 
 let sig_item config init_fct state s =
diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index f03141a2..19cd0649 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -35,6 +35,7 @@ type W.kind +=
   | Returned_tuple of string
   | Ghost_values of (string * [ `Arg | `Ret ])
   | Incompatible_sut of string
+  | Incomplete_ret_val_computation of string
 
 let level kind =
   match kind with
@@ -42,7 +43,8 @@ let level kind =
   | Multiple_sut_arguments _ | Incompatible_type _ | No_spec _
   | Impossible_term_substitution _ | Ignored_modifies
   | Ensures_not_found_for_next_state _ | Type_not_supported _
-  | Functional_argument _ | Returned_tuple _ | Ghost_values _ ->
+  | Functional_argument _ | Returned_tuple _ | Ghost_values _
+  | Incomplete_ret_val_computation _ ->
       W.Warning
   | No_sut_type _ | No_init_function _ | Syntax_error_in_type _
   | Sut_type_not_supported _ | Type_not_supported_for_sut_parameter _
@@ -216,6 +218,12 @@ let pp_kind ppf kind =
         "the declaration of the SUT type is incompatible with the configured \
          one: "
         t
+  | Incomplete_ret_val_computation fct ->
+      pf ppf
+        "Incomplete computation of the returned value in the specification of \
+         %s. Failure message won't be able to display the expected returned \
+         value"
+        fct
   | _ -> W.pp_kind ppf kind
 
 let pp_errors = W.pp_param pp_kind level |> Fmt.list
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index a716a6dd..02756ce4 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -35,6 +35,7 @@ type W.kind +=
   | Returned_tuple of string
   | Ghost_values of (string * [ `Arg | `Ret ])
   | Incompatible_sut of string
+  | Incomplete_ret_val_computation of string
 
 type 'a reserr
 
diff --git a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml
index a3b453a3..b1c9cd66 100644
--- a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml
+++ b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml
@@ -1,27 +1,53 @@
 open STM
 include Ortac_runtime
 
-type report = { cmd : string; terms : (string * location) list }
+type report = {
+  mod_name : string;
+  init_sut : string;
+  ret : res option;
+  cmd : string;
+  terms : (string * location) list;
+}
 
-let report cmd terms = { cmd; terms }
+let report mod_name init_sut ret cmd terms =
+  { mod_name; init_sut; ret; cmd; terms }
 
 let append a b =
   match (a, b) with
   | None, None -> None
   | Some _, None -> a
   | None, Some _ -> b
-  | Some { cmd = cmd0; terms = terms0 }, Some { cmd = cmd1; terms = terms1 } ->
-      assert (cmd0 = cmd1);
-      Some (report cmd0 (terms0 @ terms1))
+  | Some r0, Some r1 ->
+      assert (r0.cmd = r1.cmd);
+      Some { r0 with terms = r0.terms @ r1.terms }
+
+type _ ty += Dummy : _ ty
+
+let dummy = (Dummy, fun _ -> Printf.sprintf "unknown value")
+let is_dummy = function Res ((Dummy, _), _) -> true | _ -> false
 
 module Make (Spec : Spec) = struct
   open QCheck
   module Internal = Internal.Make (Spec) [@alert "-internal"]
 
-  let pp_trace ppf trace =
+  let pp_trace ppf (trace, mod_name, init_sut, ret) =
     let open Fmt in
-    let pp_aux ppf (c, r) = pf ppf "%s : %s" (Spec.show_cmd c) (show_res r) in
-    pf ppf "@[%a@]" (list ~sep:(any "@\n") pp_aux) trace
+    let pp_expected ppf = function
+      | Some ret when not @@ is_dummy ret ->
+          pf ppf "assert (r = %s)@\n" (show_res ret)
+      | _ -> ()
+    in
+    let rec aux ppf = function
+      | [ (c, r) ] ->
+          pf ppf "let r = %s@\n%a(* returned %s *)@\n" (Spec.show_cmd c)
+            pp_expected ret (show_res r)
+      | (c, r) :: xs ->
+          pf ppf "let _ = %s@\n(* returned %s *)@\n" (Spec.show_cmd c)
+            (show_res r);
+          aux ppf xs
+      | _ -> assert false
+    in
+    pf ppf "@[open %s@\nlet sut = %s@\n%a@]" mod_name init_sut aux trace
 
   let pp_terms ppf err =
     let open Fmt in
@@ -35,7 +61,8 @@ module Make (Spec : Spec) = struct
       \  @[%a@]@\n\
        when executing the following sequence of operations:@\n\
        @;\
-      \  @[%a@]@." report.cmd pp_terms report.terms pp_trace trace
+      \  @[%a@]@." report.cmd pp_terms report.terms pp_trace
+      (trace, report.mod_name, report.init_sut, report.ret)
 
   let rec check_disagree postcond s sut cs =
     match cs with
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 06c665d2..01b57bcc 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -9,6 +9,7 @@ let pat_default = ppat_construct (lident "Char") None
 let exp_default = evar "char"
 let res_default = Ident.create ~loc:Location.none "res"
 let list_append = list_fold_expr (qualify [ "Ortac_runtime" ] "append") "None"
+let res = lident "Res"
 
 let may_raise_exception v =
   match (v.postcond.exceptional, v.postcond.checks) with
@@ -272,7 +273,6 @@ let run_case config sut_name value =
   let lhs = mk_cmd_pattern value in
   let open Reserr in
   let* rhs =
-    let res = lident "Res" in
     let* ty_show = exp_of_core_type value.inst (Ir.get_return_type value) in
     let ty_show =
       if may_raise_exception value then
@@ -420,6 +420,30 @@ let precond config ir =
   in
   pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok
 
+let expected_returned_value translate_postcond value =
+  let open Reserr in
+  let ty_ret = Ir.get_return_type value in
+  let ret_val =
+    match (ty_ret.ptyp_desc, value.ret_values) with
+    | Ptyp_constr ({ txt = Lident "unit"; _ }, _), _ -> Some eunit
+    | Ptyp_tuple _, _ ->
+        failwith
+          "shouldn't happen (functions returning tuples are filtered out \
+           before)"
+    | _, [ xs ] ->
+        Option.bind
+          (to_option @@ map translate_postcond xs)
+          (Fun.flip List.nth_opt 0)
+    (* type of the returned value will be checked later with a proper error *)
+    | _, _ -> None
+  in
+  let ty_show = to_option @@ exp_of_core_type value.inst ty_ret in
+  match (ty_show, ret_val) with
+  | Some ty_show, Some ret_value ->
+      let args = pexp_tuple_opt [ ty_show; ret_value ] in
+      Some (pexp_construct res args)
+  | _, _ -> None
+
 let postcond_case config state invariants idx state_ident new_state_ident value
     =
   let open Reserr in
@@ -431,7 +455,25 @@ let postcond_case config state invariants idx state_ident new_state_ident value
     subst_term state ~gos_t:id ~old_t:None ~new_t:(Some new_state_ident)
       ~new_lz:true t.term
     >>= ocaml_of_term config
-  and wrap_check t e =
+  and dummy =
+    let ty_show = qualify [ "Ortac_runtime" ] "dummy" and value = eunit in
+    let args = pexp_tuple_opt [ ty_show; value ] in
+    pexp_construct res args
+  in
+  let* ret_val =
+    (* simply warn the user if we can't compute the expected returned value,
+       don't skip the function *)
+    match expected_returned_value translate_postcond value with
+    | None ->
+        let* () =
+          warn
+            ( Incomplete_ret_val_computation (Fmt.str "%a" Ident.pp value.id),
+              value.id.id_loc )
+        in
+        ok @@ esome dummy
+    | Some e -> ok @@ esome e
+  in
+  let wrap_check ?(normal = false) t e =
     let term = estring t.text
     and cmd = Fmt.str "%a" Ident.pp value.id |> estring
     and l = t.Ir.term.Gospel.Tterm.t_loc |> elocation in
@@ -440,7 +482,15 @@ let postcond_case config state invariants idx state_ident new_state_ident value
          (esome
          @@ pexp_apply
               (qualify [ "Ortac_runtime" ] "report")
-              [ (Nolabel, cmd); (Nolabel, elist [ pexp_tuple [ term; l ] ]) ]))
+              [
+                ( Nolabel,
+                  estring @@ Ortac_core.Context.module_name config.context );
+                (Nolabel, estring config.init_sut_txt);
+                (* we report the expected returned value only for normal behaviour *)
+                (Nolabel, if normal then ret_val else enone);
+                (Nolabel, cmd);
+                (Nolabel, elist [ pexp_tuple [ term; l ] ]);
+              ]))
   in
   let idx = List.sort Int.compare idx in
   let lhs0 = mk_cmd_pattern value in
@@ -491,11 +541,15 @@ let postcond_case config state invariants idx state_ident new_state_ident value
       in
       aux idx value.postcond.normal
     in
-    let* postcond = map (fun t -> wrap_check t <$> translate_postcond t) normal
+    (* [postcond] and [invariants] are specification of normal behaviour *)
+    let* postcond =
+      map (fun t -> wrap_check ~normal:true t <$> translate_postcond t) normal
     and* invariants =
       Option.fold ~none:(ok [])
         ~some:(fun (id, xs) ->
-          map (fun t -> wrap_check t <$> translate_invariants id t) xs)
+          map
+            (fun t -> wrap_check ~normal:true t <$> translate_invariants id t)
+            xs)
         invariants
     in
     list_append (postcond @ invariants) |> ok
@@ -651,7 +705,7 @@ let cmd_type ir =
   in
   pstr_type Recursive [ td ]
 
-let pp_cmd_case value =
+let pp_cmd_case config value =
   let lhs = mk_cmd_pattern value in
   let qualify_pp = qualify [ "Util"; "Pp" ] in
   let get_name =
@@ -676,18 +730,25 @@ let pp_cmd_case value =
   in
   let* rhs =
     let name = str_of_ident value.id in
-    let* pp_args =
-      concat_map
-        (fun (ty, id) ->
+    let rec aux ty args =
+      match (ty.ptyp_desc, args) with
+      | Ptyp_arrow (_, l, r), xs when Cfg.is_sut config l ->
+          let* fmt, pps = aux r xs in
+          ok ("sut" :: fmt, pps)
+      | Ptyp_arrow (_, _, r), (ty, id) :: xs ->
           let ty = subst_core_type value.inst ty in
-          let* pp = pp_of_ty ty in
-          ok [ pexp_apply pp [ (Nolabel, ebool true) ]; get_name id ])
-        value.args
-    in
-    let fmt =
-      String.concat " " ("%s" :: List.map (Fun.const "%a") value.args)
-      |> estring
+          let* pp = pp_of_ty ty and* fmt, pps = aux r xs in
+          ok
+            ( "%a" :: fmt,
+              pexp_apply pp [ (Nolabel, ebool true) ] :: get_name id :: pps )
+      | _, [] -> ok ([], [])
+      | _, _ ->
+          failwith
+            "shouldn't happen (list of arguments should be consistent with \
+             type)"
     in
+    let* fmt, pp_args = aux value.ty value.args in
+    let fmt = String.concat " " ("%s" :: fmt) |> estring in
     let args =
       List.map (fun x -> (Nolabel, x)) (fmt :: estring name :: pp_args)
     in
@@ -695,10 +756,10 @@ let pp_cmd_case value =
   in
   case ~lhs ~guard:None ~rhs |> ok
 
-let cmd_show ir =
+let cmd_show config ir =
   let cmd_name = gen_symbol ~prefix:"cmd" () in
   let open Reserr in
-  let* cases = map pp_cmd_case ir.values in
+  let* cases = map (pp_cmd_case config) ir.values in
   let body = pexp_match (evar cmd_name) cases in
   let pat = pvar "show_cmd" in
   let expr = efun [ (Nolabel, pvar cmd_name) ] body in
@@ -854,7 +915,7 @@ let stm include_ config ir =
   in
   let sut = sut_type config in
   let cmd = cmd_type ir in
-  let* cmd_show = cmd_show ir in
+  let* cmd_show = cmd_show config ir in
   let state = state_type ir in
   let* idx, next_state = next_state config ir in
   let* postcond = postcond config idx ir in
diff --git a/plugins/qcheck-stm/test/all_warnings_errors.expected b/plugins/qcheck-stm/test/all_warnings_errors.expected
index 81df1242..55ada85b 100644
--- a/plugins/qcheck-stm/test/all_warnings_errors.expected
+++ b/plugins/qcheck-stm/test/all_warnings_errors.expected
@@ -68,10 +68,32 @@ Warning: Skipping term_refer_to_returned_value_next_state: model contents is
          was found. Specifications should contain at least one "ensures
          x.contents = expr" where x is the SUT and expr can refer to the SUT
          only under an old operator and can't refer to the returned value.
+File "all_warnings.mli", line 39, characters 0-66:
+39 | val type_not_supported : 'a t -> s
+40 | (*@ s = type_not_supported t *)
+Warning: Incomplete computation of the returned value in the specification of type_not_supported. Failure message won't be able to display the expected returned value.
+File "all_warnings.mli", line 51, characters 0-140:
+51 | val unsupported_quantification : 'a t -> bool
+52 | (*@ b = unsupported_quantification t
+53 |     ensures b = forall a. List.mem a t.contents -> p a *)
+Warning: Incomplete computation of the returned value in the specification of unsupported_quantification. Failure message won't be able to display the expected returned value.
 File "all_warnings.mli", line 53, characters 16-54:
 53 |     ensures b = forall a. List.mem a t.contents -> p a *)
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping clause: unsupported quantification.
+File "all_warnings.mli", line 55, characters 0-111:
+55 | val record_not_model_field : 'a t -> bool
+56 | (*@ b = record_not_model_field t
+57 |     requires Array.length t.v > 0 *)
+Warning: Incomplete computation of the returned value in the specification of record_not_model_field. Failure message won't be able to display the expected returned value.
+File "all_warnings.mli", line 62, characters 0-278:
+62 | val term_refer_to_returned_value_next_state : 'a t -> 'a option
+63 | (*@ o = term_refer_to_returned_value_next_state t
+64 |     modifies t.contents
+65 |     ensures t.contents = match o with
+66 |                         | None -> old t.contents
+67 |                         | Some _ -> old t.contents *)
+Warning: Incomplete computation of the returned value in the specification of term_refer_to_returned_value_next_state. Failure message won't be able to display the expected returned value.
 File "all_warnings.mli", line 57, characters 26-29:
 57 |     requires Array.length t.v > 0 *)
                                ^^^
diff --git a/plugins/qcheck-stm/test/array_errors.expected b/plugins/qcheck-stm/test/array_errors.expected
index e69de29b..6e8d89c1 100644
--- a/plugins/qcheck-stm/test/array_errors.expected
+++ b/plugins/qcheck-stm/test/array_errors.expected
@@ -0,0 +1,5 @@
+File "array.mli", line 38, characters 0-85:
+38 | val mem : 'a -> 'a t -> bool
+39 | (*@ b = mem a t
+40 |     ensures b = List.mem a t.contents *)
+Warning: Incomplete computation of the returned value in the specification of mem. Failure message won't be able to display the expected returned value.
diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
index 5a5c22cd..e8bd1145 100644
--- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
@@ -16,16 +16,17 @@ module Spec =
       | Mem of char 
     let show_cmd cmd__001_ =
       match cmd__001_ with
-      | Length -> Format.asprintf "%s" "length"
-      | Get i -> Format.asprintf "%s %a" "get" (Util.Pp.pp_int true) i
+      | Length -> Format.asprintf "%s sut" "length"
+      | Get i -> Format.asprintf "%s sut %a" "get" (Util.Pp.pp_int true) i
       | Set (i_1, a_1) ->
-          Format.asprintf "%s %a %a" "set" (Util.Pp.pp_int true) i_1
+          Format.asprintf "%s sut %a %a" "set" (Util.Pp.pp_int true) i_1
             (Util.Pp.pp_char true) a_1
       | Fill (i_2, j, a_2) ->
-          Format.asprintf "%s %a %a %a" "fill" (Util.Pp.pp_int true) i_2
+          Format.asprintf "%s sut %a %a %a" "fill" (Util.Pp.pp_int true) i_2
             (Util.Pp.pp_int true) j (Util.Pp.pp_char true) a_2
-      | To_list -> Format.asprintf "%s" "to_list"
-      | Mem a_3 -> Format.asprintf "%s %a" "mem" (Util.Pp.pp_char true) a_3
+      | To_list -> Format.asprintf "%s sut" "to_list"
+      | Mem a_3 ->
+          Format.asprintf "%s %a sut" "mem" (Util.Pp.pp_char true) a_3
     type nonrec state = {
       size: int ;
       contents: char list }
@@ -363,7 +364,32 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
           then None
           else
             Some
-              (Ortac_runtime.report "length"
+              (Ortac_runtime.report "Array" "make 16 'a'"
+                 (Some
+                    (Res
+                       (int,
+                         (try (Lazy.force new_state__011_).size
+                          with
+                          | e ->
+                              raise
+                                (Ortac_runtime.Partial_function
+                                   (e,
+                                     {
+                                       Ortac_runtime.start =
+                                         {
+                                           pos_fname = "array.mli";
+                                           pos_lnum = 7;
+                                           pos_bol = 238;
+                                           pos_cnum = 254
+                                         };
+                                       Ortac_runtime.stop =
+                                         {
+                                           pos_fname = "array.mli";
+                                           pos_lnum = 7;
+                                           pos_bol = 238;
+                                           pos_cnum = 260
+                                         }
+                                     })))))) "length"
                  [("i = t.size",
                     {
                       Ortac_runtime.start =
@@ -418,7 +444,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "get"
+                     (Ortac_runtime.report "Array" "make 16 'a'" None "get"
                         [("0 <= i < t.size",
                            {
                              Ortac_runtime.start =
@@ -470,7 +496,36 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "get"
+                        (Ortac_runtime.report "Array" "make 16 'a'"
+                           (Some
+                              (Res
+                                 (char,
+                                   (try
+                                      Ortac_runtime.Gospelstdlib.List.nth
+                                        (Lazy.force new_state__011_).contents
+                                        (Ortac_runtime.Gospelstdlib.integer_of_int
+                                           i)
+                                    with
+                                    | e ->
+                                        raise
+                                          (Ortac_runtime.Partial_function
+                                             (e,
+                                               {
+                                                 Ortac_runtime.start =
+                                                   {
+                                                     pos_fname = "array.mli";
+                                                     pos_lnum = 12;
+                                                     pos_bol = 405;
+                                                     pos_cnum = 421
+                                                   };
+                                                 Ortac_runtime.stop =
+                                                   {
+                                                     pos_fname = "array.mli";
+                                                     pos_lnum = 12;
+                                                     pos_bol = 405;
+                                                     pos_cnum = 442
+                                                   }
+                                               })))))) "get"
                            [("a = List.nth t.contents i",
                               {
                                 Ortac_runtime.start =
@@ -529,7 +584,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "get"
+                        (Ortac_runtime.report "Array" "make 16 'a'" None
+                           "get"
                            [("0 <= i < t.size",
                               {
                                 Ortac_runtime.start =
@@ -584,7 +640,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "set"
+                     (Ortac_runtime.report "Array" "make 16 'a'" None "set"
                         [("0 <= i < t.size",
                            {
                              Ortac_runtime.start =
@@ -644,7 +700,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "set"
+                        (Ortac_runtime.report "Array" "make 16 'a'" None
+                           "set"
                            [("0 <= i < t.size",
                               {
                                 Ortac_runtime.start =
@@ -693,7 +750,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "fill"
+                        (Ortac_runtime.report "Array" "make 16 'a'" None
+                           "fill"
                            [("0 <= i",
                               {
                                 Ortac_runtime.start =
@@ -741,7 +799,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                        then None
                        else
                          Some
-                           (Ortac_runtime.report "fill"
+                           (Ortac_runtime.report "Array" "make 16 'a'" None
+                              "fill"
                               [("0 <= j",
                                  {
                                    Ortac_runtime.start =
@@ -792,7 +851,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                        then None
                        else
                          Some
-                           (Ortac_runtime.report "fill"
+                           (Ortac_runtime.report "Array" "make 16 'a'" None
+                              "fill"
                               [("i + j <= t.size",
                                  {
                                    Ortac_runtime.start =
@@ -846,7 +906,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                        then None
                        else
                          Some
-                           (Ortac_runtime.report "fill"
+                           (Ortac_runtime.report "Array" "make 16 'a'" None
+                              "fill"
                               [("0 <= i",
                                  {
                                    Ortac_runtime.start =
@@ -894,7 +955,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                           then None
                           else
                             Some
-                              (Ortac_runtime.report "fill"
+                              (Ortac_runtime.report "Array" "make 16 'a'"
+                                 None "fill"
                                  [("0 <= j",
                                     {
                                       Ortac_runtime.start =
@@ -946,7 +1008,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                           then None
                           else
                             Some
-                              (Ortac_runtime.report "fill"
+                              (Ortac_runtime.report "Array" "make 16 'a'"
+                                 None "fill"
                                  [("i + j <= t.size",
                                     {
                                       Ortac_runtime.start =
@@ -991,7 +1054,32 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
           then None
           else
             Some
-              (Ortac_runtime.report "to_list"
+              (Ortac_runtime.report "Array" "make 16 'a'"
+                 (Some
+                    (Res
+                       ((list char),
+                         (try (Lazy.force new_state__011_).contents
+                          with
+                          | e ->
+                              raise
+                                (Ortac_runtime.Partial_function
+                                   (e,
+                                     {
+                                       Ortac_runtime.start =
+                                         {
+                                           pos_fname = "array.mli";
+                                           pos_lnum = 36;
+                                           pos_bol = 1559;
+                                           pos_cnum = 1575
+                                         };
+                                       Ortac_runtime.stop =
+                                         {
+                                           pos_fname = "array.mli";
+                                           pos_lnum = 36;
+                                           pos_bol = 1559;
+                                           pos_cnum = 1585
+                                         }
+                                     })))))) "to_list"
                  [("l = t.contents",
                     {
                       Ortac_runtime.start =
@@ -1039,7 +1127,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
           then None
           else
             Some
-              (Ortac_runtime.report "mem"
+              (Ortac_runtime.report "Array" "make 16 'a'"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "mem"
                  [("b = List.mem a t.contents",
                     {
                       Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
index 5a4c7ed6..d1535b51 100644
--- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
@@ -37,7 +37,7 @@ module Spec =
     let show_cmd cmd__001_ =
       match cmd__001_ with
       | Set (i_1, a_2) ->
-          Format.asprintf "%s %a %a" "set" (Util.Pp.pp_int true) i_1
+          Format.asprintf "%s sut %a %a" "set" (Util.Pp.pp_int true) i_1
             (Util.Pp.pp_char true) a_2
     type nonrec state = {
       contents: char list }
@@ -199,7 +199,8 @@ let ortac_postcond cmd__006_ state__007_ res__008_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "set"
+                     (Ortac_runtime.report "Conjunctive_clauses"
+                        "make 42 'a'" None "set"
                         [("0 <= i < List.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -259,7 +260,8 @@ let ortac_postcond cmd__006_ state__007_ res__008_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "set"
+                        (Ortac_runtime.report "Conjunctive_clauses"
+                           "make 42 'a'" None "set"
                            [("0 <= i < List.length t.contents",
                               {
                                 Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/hashtbl_errors.expected b/plugins/qcheck-stm/test/hashtbl_errors.expected
index 66a3dfee..05e6eee9 100644
--- a/plugins/qcheck-stm/test/hashtbl_errors.expected
+++ b/plugins/qcheck-stm/test/hashtbl_errors.expected
@@ -115,7 +115,36 @@ File "hashtbl.mli", line 106, characters 0-54:
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping seeded_hash_param: functions without specifications cannot
          be tested.
+File "hashtbl.mli", line 28, characters 0-226:
+28 | val find : ('a, 'b) t -> 'a -> 'b
+29 | (*@ b = find h a
+30 |     raises Not_found -> forall x. not (List.mem (a, x) h.contents)
+31 |     raises Not_found -> not (List.mem a (List.map fst h.contents))
+32 |     ensures List.mem (a, b) h.contents *)
+Warning: Incomplete computation of the returned value in the specification of find. Failure message won't be able to display the expected returned value.
 File "hashtbl.mli", line 30, characters 24-66:
 30 |     raises Not_found -> forall x. not (List.mem (a, x) h.contents)
                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping clause: unsupported quantification.
+File "hashtbl.mli", line 34, characters 0-197:
+34 | val find_opt : ('a, 'b) t -> 'a -> 'b option
+35 | (*@ o = find_opt h a
+36 |     ensures match o with
+37 |       | None -> not (List.mem a (List.map fst h.contents))
+38 |       | Some b -> List.mem (a, b) h.contents *)
+Warning: Incomplete computation of the returned value in the specification of find_opt. Failure message won't be able to display the expected returned value.
+File "hashtbl.mli", line 40, characters 0-162:
+40 | val find_all : ('a, 'b) t -> 'a -> 'b list
+41 | (*@ bs = find_all h a
+42 |     ensures bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents *)
+Warning: Incomplete computation of the returned value in the specification of find_all. Failure message won't be able to display the expected returned value.
+File "hashtbl.mli", line 44, characters 0-106:
+44 | val mem : ('a, 'b) t -> 'a -> bool
+45 | (*@ b = mem h a
+46 |     ensures b = List.mem a (List.map fst h.contents) *)
+Warning: Incomplete computation of the returned value in the specification of mem. Failure message won't be able to display the expected returned value.
+File "hashtbl.mli", line 74, characters 0-89:
+74 | val length : ('a, 'b) t -> int
+75 | (*@ i = length h
+76 |     ensures i = List.length h.contents *)
+Warning: Incomplete computation of the returned value in the specification of length. Failure message won't be able to display the expected returned value.
diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
index 335b4c10..a894c788 100644
--- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
@@ -47,23 +47,25 @@ module Spec =
       | Length 
     let show_cmd cmd__001_ =
       match cmd__001_ with
-      | Clear -> Format.asprintf "%s" "clear"
-      | Reset -> Format.asprintf "%s" "reset"
+      | Clear -> Format.asprintf "%s sut" "clear"
+      | Reset -> Format.asprintf "%s sut" "reset"
       | Add (a_2, b_2) ->
-          Format.asprintf "%s %a %a" "add" (Util.Pp.pp_char true) a_2
+          Format.asprintf "%s sut %a %a" "add" (Util.Pp.pp_char true) a_2
             (Util.Pp.pp_int true) b_2
-      | Find a_3 -> Format.asprintf "%s %a" "find" (Util.Pp.pp_char true) a_3
+      | Find a_3 ->
+          Format.asprintf "%s sut %a" "find" (Util.Pp.pp_char true) a_3
       | Find_opt a_4 ->
-          Format.asprintf "%s %a" "find_opt" (Util.Pp.pp_char true) a_4
+          Format.asprintf "%s sut %a" "find_opt" (Util.Pp.pp_char true) a_4
       | Find_all a_5 ->
-          Format.asprintf "%s %a" "find_all" (Util.Pp.pp_char true) a_5
-      | Mem a_6 -> Format.asprintf "%s %a" "mem" (Util.Pp.pp_char true) a_6
+          Format.asprintf "%s sut %a" "find_all" (Util.Pp.pp_char true) a_5
+      | Mem a_6 ->
+          Format.asprintf "%s sut %a" "mem" (Util.Pp.pp_char true) a_6
       | Remove a_7 ->
-          Format.asprintf "%s %a" "remove" (Util.Pp.pp_char true) a_7
+          Format.asprintf "%s sut %a" "remove" (Util.Pp.pp_char true) a_7
       | Replace (a_8, b_3) ->
-          Format.asprintf "%s %a %a" "replace" (Util.Pp.pp_char true) a_8
+          Format.asprintf "%s sut %a %a" "replace" (Util.Pp.pp_char true) a_8
             (Util.Pp.pp_int true) b_3
-      | Length -> Format.asprintf "%s" "length"
+      | Length -> Format.asprintf "%s sut" "length"
     type nonrec state = {
       contents: (char * int) list }
     let init_state =
@@ -318,7 +320,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "find"
+                   (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
+                      (Some (Res (Ortac_runtime.dummy, ()))) "find"
                       [("List.mem (a, b) h.contents",
                          {
                            Ortac_runtime.start =
@@ -368,7 +371,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "find"
+                   (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
+                      None "find"
                       [("not (List.mem a (List.map fst h.contents))",
                          {
                            Ortac_runtime.start =
@@ -431,7 +435,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           then None
           else
             Some
-              (Ortac_runtime.report "find_opt"
+              (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "find_opt"
                  [("match o with\n      | None -> not (List.mem a (List.map fst h.contents))\n      | Some b -> List.mem (a, b) h.contents",
                     {
                       Ortac_runtime.start =
@@ -481,7 +486,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           then None
           else
             Some
-              (Ortac_runtime.report "find_all"
+              (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "find_all"
                  [("bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents",
                     {
                       Ortac_runtime.start =
@@ -531,7 +537,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           then None
           else
             Some
-              (Ortac_runtime.report "mem"
+              (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "mem"
                  [("b = List.mem a (List.map fst h.contents)",
                     {
                       Ortac_runtime.start =
@@ -581,7 +588,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           then None
           else
             Some
-              (Ortac_runtime.report "length"
+              (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
                  [("i = List.length h.contents",
                     {
                       Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml
index fcf667ad..21b544cf 100644
--- a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml
@@ -11,7 +11,8 @@ module Spec =
       | Push of int 
     let show_cmd cmd__001_ =
       match cmd__001_ with
-      | Push a_1 -> Format.asprintf "%s %a" "push" (Util.Pp.pp_int true) a_1
+      | Push a_1 ->
+          Format.asprintf "%s %a sut" "push" (Util.Pp.pp_int true) a_1
     type nonrec state = {
       contents: int list }
     let init_state =
@@ -148,7 +149,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           then None
           else
             Some
-              (Ortac_runtime.report "push"
+              (Ortac_runtime.report "Invariants" "create 42"
+                 (Some (Res (unit, ()))) "push"
                  [("List.length x.contents > 0",
                     {
                       Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/record_errors.expected b/plugins/qcheck-stm/test/record_errors.expected
index 2ca04f5c..6f13fc75 100644
--- a/plugins/qcheck-stm/test/record_errors.expected
+++ b/plugins/qcheck-stm/test/record_errors.expected
@@ -6,6 +6,15 @@ File "record.mli", line 15, characters 12-22:
 15 | val plus2 : int -> int
                  ^^^^^^^^^^
 Warning: Skipping plus2: functions with no SUT argument cannot be tested.
+File "record.mli", line 20, characters 0-144:
+20 | val get : t -> int
+21 | (*@ i = get r
+22 |     pure
+23 |     ensures i = r.value
+24 |     ensures i = r.c
+25 |     ensures plus1 i = i + 1
+26 |     ensures plus2 i = i + 2 *)
+Warning: Incomplete computation of the returned value in the specification of get. Failure message won't be able to display the expected returned value.
 File "record.mli", line 24, characters 16-19:
 24 |     ensures i = r.c
                      ^^^
diff --git a/plugins/qcheck-stm/test/record_stm_tests.expected.ml b/plugins/qcheck-stm/test/record_stm_tests.expected.ml
index e05824d3..56839571 100644
--- a/plugins/qcheck-stm/test/record_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/record_stm_tests.expected.ml
@@ -35,7 +35,7 @@ module Spec =
     type cmd =
       | Get 
     let show_cmd cmd__001_ =
-      match cmd__001_ with | Get -> Format.asprintf "%s" "get"
+      match cmd__001_ with | Get -> Format.asprintf "%s sut" "get"
     type nonrec state = {
       value: Ortac_runtime.integer }
     let init_state =
@@ -114,7 +114,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
              then None
              else
                Some
-                 (Ortac_runtime.report "get"
+                 (Ortac_runtime.report "Record" "make 42"
+                    (Some (Res (Ortac_runtime.dummy, ()))) "get"
                     [("i = r.value",
                        {
                          Ortac_runtime.start =
@@ -164,7 +165,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                 then None
                 else
                   Some
-                    (Ortac_runtime.report "get"
+                    (Ortac_runtime.report "Record" "make 42"
+                       (Some (Res (Ortac_runtime.dummy, ()))) "get"
                        [("plus1 i = i + 1",
                           {
                             Ortac_runtime.start =
@@ -212,7 +214,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                 then None
                 else
                   Some
-                    (Ortac_runtime.report "get"
+                    (Ortac_runtime.report "Record" "make 42"
+                       (Some (Res (Ortac_runtime.dummy, ()))) "get"
                        [("plus2 i = i + 2",
                           {
                             Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/ref_errors.expected b/plugins/qcheck-stm/test/ref_errors.expected
index 4dc8c349..b11e35f5 100644
--- a/plugins/qcheck-stm/test/ref_errors.expected
+++ b/plugins/qcheck-stm/test/ref_errors.expected
@@ -1,3 +1,10 @@
+File "ref.mli", line 8, characters 0-96:
+ 8 | val get : t -> int
+ 9 | (*@ i = get r
+10 |     pure
+11 |     ensures i = r.value
+12 |     ensures i + 1 = succ !r *)
+Warning: Incomplete computation of the returned value in the specification of get. Failure message won't be able to display the expected returned value.
 File "ref.mli", line 12, characters 26-27:
 12 |     ensures i + 1 = succ !r *)
                                ^
diff --git a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
index 393d67ee..67427a8a 100644
--- a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
@@ -10,7 +10,7 @@ module Spec =
     type cmd =
       | Get 
     let show_cmd cmd__001_ =
-      match cmd__001_ with | Get -> Format.asprintf "%s" "get"
+      match cmd__001_ with | Get -> Format.asprintf "%s sut" "get"
     type nonrec state = {
       value: Ortac_runtime.integer }
     let init_state =
@@ -88,7 +88,8 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           then None
           else
             Some
-              (Ortac_runtime.report "get"
+              (Ortac_runtime.report "Ref" "make 42"
+                 (Some (Res (Ortac_runtime.dummy, ()))) "get"
                  [("i = r.value",
                     {
                       Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/sequence_model_errors.expected b/plugins/qcheck-stm/test/sequence_model_errors.expected
index e69de29b..643f43a9 100644
--- a/plugins/qcheck-stm/test/sequence_model_errors.expected
+++ b/plugins/qcheck-stm/test/sequence_model_errors.expected
@@ -0,0 +1,16 @@
+File "sequence_model.mli", line 17, characters 0-253:
+17 | val remove : 'a t -> 'a option
+18 | (*@ o = remove t
+19 |     modifies t.contents
+20 |     ensures t.contents = match Sequence.length (old t.contents) with
+21 |                           | 0 -> Sequence.empty
+22 |                           | _ -> Sequence.tl (old t.contents) *)
+Warning: Incomplete computation of the returned value in the specification of remove. Failure message won't be able to display the expected returned value.
+File "sequence_model.mli", line 24, characters 0-255:
+24 | val remove_ : 'a t -> 'a option
+25 | (*@ o = remove_ t
+26 |     modifies t.contents
+27 |     ensures t.contents = match length_opt (old t.contents) with
+28 |                           | Some 0 -> Sequence.empty
+29 |                           | _ -> Sequence.tl (old t.contents) *)
+Warning: Incomplete computation of the returned value in the specification of remove_. Failure message won't be able to display the expected returned value.
diff --git a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml
index 9a679d8b..1237bd48 100644
--- a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml
@@ -36,9 +36,9 @@ module Spec =
       | Remove_ 
     let show_cmd cmd__001_ =
       match cmd__001_ with
-      | Add v -> Format.asprintf "%s %a" "add" (Util.Pp.pp_char true) v
-      | Remove -> Format.asprintf "%s" "remove"
-      | Remove_ -> Format.asprintf "%s" "remove_"
+      | Add v -> Format.asprintf "%s %a sut" "add" (Util.Pp.pp_char true) v
+      | Remove -> Format.asprintf "%s sut" "remove"
+      | Remove_ -> Format.asprintf "%s sut" "remove_"
     type nonrec state = {
       contents: char Ortac_runtime.Gospelstdlib.sequence }
     let init_state =