diff --git a/CHANGES.md b/CHANGES.md
index ef7d25d8..26092b04 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,7 +2,8 @@
 
 - Improve test-failure message
   [\#202](https://github.com/ocaml-gospel/ortac/pull/202) and
-  [\#204](https://github.com/ocaml-gospel/ortac/pull/204)
+  [\#204](https://github.com/ocaml-gospel/ortac/pull/204) and
+  [\#206](https://github.com/ocaml-gospel/ortac/pull/206)
 - 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 a5898fd7..099ae07b 100644
--- a/examples/lwt_dllist_tests.ml
+++ b/examples/lwt_dllist_tests.ml
@@ -337,7 +337,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           else
             Some
               (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "is_empty"
                  [("b <-> s.contents = Sequence.empty",
                     {
                       Ortac_runtime.start =
@@ -386,7 +386,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           else
             Some
               (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "length"
                  [("l = Sequence.length s.contents",
                     {
                       Ortac_runtime.start =
@@ -444,7 +444,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                else
                  Some
                    (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
-                      (Some (Res (Ortac_runtime.dummy, ()))) "take_l"
+                      (Either.right (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 =
@@ -496,8 +496,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()" None
-                      "take_l"
+                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                      (Either.left "Empty") "take_l"
                       [("old s.contents = Sequence.empty = s.contents",
                          {
                            Ortac_runtime.start =
@@ -558,7 +558,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                else
                  Some
                    (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
-                      (Some (Res (Ortac_runtime.dummy, ()))) "take_r"
+                      (Either.right (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 =
@@ -610,8 +610,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()" None
-                      "take_r"
+                   (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
+                      (Either.left "Empty") "take_r"
                       [("old s.contents = Sequence.empty = s.contents",
                          {
                            Ortac_runtime.start =
@@ -664,7 +664,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           else
             Some
               (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "take_opt_l"
+                 (Either.right (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 =
@@ -716,7 +716,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
           else
             Some
               (Ortac_runtime.report "Lwt_dllist_spec" "create ()"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "take_opt_r"
+                 (Either.right (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 5512bf91..c7937aff 100644
--- a/examples/varray_circular_tests.ml
+++ b/examples/varray_circular_tests.ml
@@ -763,7 +763,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                else
                  Some
                    (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
-                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_back"
+                      (Either.right (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 =
@@ -816,7 +817,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                else
                  Some
                    (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
-                      None "pop_back"
+                      (Either.left "Not_found") "pop_back"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -874,7 +875,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                else
                  Some
                    (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
-                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_front"
+                      (Either.right (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 =
@@ -927,7 +929,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                else
                  Some
                    (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
-                      None "pop_front"
+                      (Either.left "Not_found") "pop_front"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -984,7 +986,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  else
                    Some
                      (Ortac_runtime.report "Varray_circular_spec"
-                        "make 42 'a'" None "insert_at"
+                        "make 42 'a'" (Either.left "Invalid_argument")
+                        "insert_at"
                         [("0 <= i <= Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1047,7 +1050,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
-                           "make 42 'a'" None "insert_at"
+                           "make 42 'a'" (Either.left "Invalid_argument")
+                           "insert_at"
                            [("0 <= i <= Sequence.length t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1096,7 +1100,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  else
                    Some
                      (Ortac_runtime.report "Varray_circular_spec"
-                        "make 42 'a'" None "pop_at"
+                        "make 42 'a'" (Either.left "Invalid_argument")
+                        "pop_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1152,7 +1157,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
                            "make 42 'a'"
-                           (Some (Res (Ortac_runtime.dummy, ()))) "pop_at"
+                           (Either.right (Res (Ortac_runtime.dummy, ())))
+                           "pop_at"
                            [("(proj x) = old t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1208,7 +1214,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
-                           "make 42 'a'" None "pop_at"
+                           "make 42 'a'" (Either.left "Invalid_argument")
+                           "pop_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1257,7 +1264,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  else
                    Some
                      (Ortac_runtime.report "Varray_circular_spec"
-                        "make 42 'a'" None "delete_at"
+                        "make 42 'a'" (Either.left "Invalid_argument")
+                        "delete_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1315,7 +1323,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
-                           "make 42 'a'" (Some (Res (unit, ()))) "delete_at"
+                           "make 42 'a'" (Either.right (Res (unit, ())))
+                           "delete_at"
                            [("Sequence.length t.contents = Sequence.length (old t.contents) - 1",
                               {
                                 Ortac_runtime.start =
@@ -1371,7 +1380,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
-                           "make 42 'a'" None "delete_at"
+                           "make 42 'a'" (Either.left "Invalid_argument")
+                           "delete_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1420,7 +1430,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  else
                    Some
                      (Ortac_runtime.report "Varray_circular_spec"
-                        "make 42 'a'" None "get"
+                        "make 42 'a'" (Either.left "Invalid_argument") "get"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1476,7 +1486,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
                            "make 42 'a'"
-                           (Some (Res (Ortac_runtime.dummy, ()))) "get"
+                           (Either.right (Res (Ortac_runtime.dummy, ())))
+                           "get"
                            [("(proj x) = t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1532,7 +1543,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
-                           "make 42 'a'" None "get"
+                           "make 42 'a'" (Either.left "Invalid_argument")
+                           "get"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1581,7 +1593,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  else
                    Some
                      (Ortac_runtime.report "Varray_circular_spec"
-                        "make 42 'a'" None "set"
+                        "make 42 'a'" (Either.left "Invalid_argument") "set"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1638,7 +1650,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
-                           "make 42 'a'" None "set"
+                           "make 42 'a'" (Either.left "Invalid_argument")
+                           "set"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1687,7 +1700,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           else
             Some
               (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "length"
                  [("l = Sequence.length t.contents",
                     {
                       Ortac_runtime.start =
@@ -1736,7 +1749,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           else
             Some
               (Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "is_empty"
                  [("b <-> t.contents = Sequence.empty",
                     {
                       Ortac_runtime.start =
@@ -1800,7 +1813,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  else
                    Some
                      (Ortac_runtime.report "Varray_circular_spec"
-                        "make 42 'a'" None "fill"
+                        "make 42 'a'" (Either.left "Invalid_argument") "fill"
                         [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1873,7 +1886,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_circular_spec"
-                           "make 42 'a'" None "fill"
+                           "make 42 'a'" (Either.left "Invalid_argument")
+                           "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 a4da974d..5afd33ac 100644
--- a/examples/varray_tests.ml
+++ b/examples/varray_tests.ml
@@ -763,7 +763,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                else
                  Some
                    (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_back"
+                      (Either.right (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 =
@@ -815,8 +816,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                      "pop_back"
+                   (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                      (Either.left "Not_found") "pop_back"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -874,7 +875,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                else
                  Some
                    (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                      (Some (Res (Ortac_runtime.dummy, ()))) "pop_front"
+                      (Either.right (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 =
@@ -926,8 +928,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                then None
                else
                  Some
-                   (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                      "pop_front"
+                   (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                      (Either.left "Not_found") "pop_front"
                       [("t.contents = old t.contents = Sequence.empty",
                          {
                            Ortac_runtime.start =
@@ -983,8 +985,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                        "insert_at"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                        (Either.left "Invalid_argument") "insert_at"
                         [("0 <= i <= Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1045,7 +1047,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           None "insert_at"
+                           (Either.left "Invalid_argument") "insert_at"
                            [("0 <= i <= Sequence.length t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1093,8 +1095,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                        "pop_at"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                        (Either.left "Invalid_argument") "pop_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1147,7 +1149,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           (Some (Res (Ortac_runtime.dummy, ()))) "pop_at"
+                           (Either.right (Res (Ortac_runtime.dummy, ())))
+                           "pop_at"
                            [("(proj x) = old t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1201,7 +1204,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           None "pop_at"
+                           (Either.left "Invalid_argument") "pop_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1249,8 +1252,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                        "delete_at"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                        (Either.left "Invalid_argument") "delete_at"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1306,7 +1309,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           (Some (Res (unit, ()))) "delete_at"
+                           (Either.right (Res (unit, ()))) "delete_at"
                            [("Sequence.length t.contents = Sequence.length (old t.contents) - 1",
                               {
                                 Ortac_runtime.start =
@@ -1360,7 +1363,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           None "delete_at"
+                           (Either.left "Invalid_argument") "delete_at"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1408,8 +1411,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                        "get"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                        (Either.left "Invalid_argument") "get"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1462,7 +1465,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           (Some (Res (Ortac_runtime.dummy, ()))) "get"
+                           (Either.right (Res (Ortac_runtime.dummy, ())))
+                           "get"
                            [("(proj x) = t.contents[i]",
                               {
                                 Ortac_runtime.start =
@@ -1516,7 +1520,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           None "get"
+                           (Either.left "Invalid_argument") "get"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1564,8 +1568,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                        "set"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                        (Either.left "Invalid_argument") "set"
                         [("inside i t.contents",
                            {
                              Ortac_runtime.start =
@@ -1620,7 +1624,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           None "set"
+                           (Either.left "Invalid_argument") "set"
                            [("inside i t.contents",
                               {
                                 Ortac_runtime.start =
@@ -1669,7 +1673,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           else
             Some
               (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "length"
                  [("l = Sequence.length t.contents",
                     {
                       Ortac_runtime.start =
@@ -1718,7 +1722,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
           else
             Some
               (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "is_empty"
                  [("b <-> t.contents = Sequence.empty",
                     {
                       Ortac_runtime.start =
@@ -1781,8 +1785,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Varray_spec" "make 42 'a'" None
-                        "fill"
+                     (Ortac_runtime.report "Varray_spec" "make 42 'a'"
+                        (Either.left "Invalid_argument") "fill"
                         [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -1853,7 +1857,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                     else
                       Some
                         (Ortac_runtime.report "Varray_spec" "make 42 'a'"
-                           None "fill"
+                           (Either.left "Invalid_argument") "fill"
                            [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
                               {
                                 Ortac_runtime.start =
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 d3badab8..34395cb4 100644
--- a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml
+++ b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml
@@ -4,7 +4,7 @@ include Ortac_runtime
 type report = {
   mod_name : string;
   init_sut : string;
-  ret : res option;
+  ret : (string, res) Either.t;
   cmd : string;
   terms : (string * location) list;
 }
@@ -33,8 +33,14 @@ module Make (Spec : Spec) = struct
   let pp_trace ppf (trace, mod_name, init_sut, ret) =
     let open Fmt in
     let pp_expected ppf = function
-      | Some ret when not @@ is_dummy ret ->
+      | Either.Right ret when not @@ is_dummy ret ->
           pf ppf "assert (r = %s)@\n" (show_res ret)
+      | Either.Left exn ->
+          pf ppf
+            "assert (@[match r with@\n\
+            \  @[| Error (%s _) -> true@\n\
+             | _ -> false@]@])@\n"
+            exn
       | _ -> ()
     in
     let rec aux ppf = function
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 8535c733..8f8561b2 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -11,6 +11,16 @@ 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 eeither case e =
+  pexp_construct (noloc (Ldot (Lident "Either", case))) (Some e)
+
+let eleft = eeither "left"
+let eright = eeither "right"
+
+let eprotect call =
+  let lazy_call = efun [ (Nolabel, punit) ] call in
+  pexp_apply (evar "protect") [ (Nolabel, lazy_call); (Nolabel, eunit) ]
+
 let may_raise_exception v =
   match (v.postcond.exceptional, v.postcond.checks) with
   | [], [] -> false
@@ -295,12 +305,7 @@ let run_case config sut_name value =
       in
       pexp_apply efun (aux value.ty (List.map snd value.args))
     in
-    let call =
-      if may_raise_exception value then
-        let lazy_call = efun [ (Nolabel, punit) ] call in
-        pexp_apply (evar "protect") [ (Nolabel, lazy_call); (Nolabel, eunit) ]
-      else call
-    in
+    let call = if may_raise_exception value then eprotect call else call in
     let args = Some (pexp_tuple [ ty_show; call ]) in
     pexp_construct res args |> ok
   in
@@ -470,13 +475,16 @@ let postcond_case config state invariants idx state_ident new_state_ident value
             ( Incomplete_ret_val_computation (Fmt.str "%a" Ident.pp value.id),
               value.id.id_loc )
         in
-        ok @@ esome dummy
-    | Some e -> ok @@ esome e
+        ok dummy
+    | Some e -> ok e
   in
-  let wrap_check ?(normal = false) t e =
+  let wrap_check ?(exn = None) 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
+    and l = t.Ir.term.Gospel.Tterm.t_loc |> elocation
+    and ret_val =
+      match exn with Some e -> eleft @@ estring e | None -> eright ret_val
+    in
     pexp_ifthenelse e enone
       (Some
          (esome
@@ -486,8 +494,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value
                 ( 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, ret_val);
                 (Nolabel, cmd);
                 (Nolabel, elist [ pexp_tuple [ term; l ] ]);
               ]))
@@ -542,14 +549,11 @@ let postcond_case config state invariants idx state_ident new_state_ident value
       aux idx value.postcond.normal
     in
     (* [postcond] and [invariants] are specification of normal behaviour *)
-    let* postcond =
-      map (fun t -> wrap_check ~normal:true t <$> translate_postcond t) normal
+    let* postcond = map (fun t -> wrap_check t <$> translate_postcond t) normal
     and* invariants =
       Option.fold ~none:(ok [])
         ~some:(fun (id, xs) ->
-          map
-            (fun t -> wrap_check ~normal:true t <$> translate_invariants id t)
-            xs)
+          map (fun t -> wrap_check t <$> translate_invariants id t) xs)
         invariants
     in
     list_append (postcond @ invariants) |> ok
@@ -574,13 +578,15 @@ let postcond_case config state invariants idx state_ident new_state_ident value
         Fun.flip ( @ ) [ case ~lhs:ppat_any ~guard:None ~rhs:enone ]
         <$> map
               (fun (x, p, t) ->
+                let xstr = Fmt.str "%a" Ident.pp x.Gospel.Ttypes.xs_ident in
                 let lhs =
-                  ppat_construct
-                    (Fmt.str "%a" Ident.pp x.Gospel.Ttypes.xs_ident |> lident)
+                  ppat_construct (lident xstr)
                     (Option.map Ortac_core.Ocaml_of_gospel.pattern p)
                 in
                 let lhs = ppat_construct (lident "Error") (Some lhs) in
-                let* rhs = wrap_check t <$> translate_postcond t in
+                let* rhs =
+                  wrap_check ~exn:(Some xstr) t <$> translate_postcond t
+                in
                 case ~lhs ~guard:None ~rhs |> ok)
               value.postcond.exceptional
       in
@@ -590,7 +596,10 @@ let postcond_case config state invariants idx state_ident new_state_ident value
   let* rhs =
     let translate_checks = translate_checks config state value state_ident in
     let* checks =
-      map (fun t -> wrap_check t <$> translate_checks t) value.postcond.checks
+      map
+        (fun t ->
+          wrap_check ~exn:(Some "Invalid_argument") t <$> translate_checks t)
+        value.postcond.checks
     in
     match checks with
     | [] -> ok rhs
diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
index 7f87209c..2be1f672 100644
--- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
@@ -368,7 +368,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
           else
             Some
               (Ortac_runtime.report "Array" "make 16 'a'"
-                 (Some
+                 (Either.right
                     (Res
                        (int,
                          (try (Lazy.force new_state__011_).size
@@ -447,7 +447,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Array" "make 16 'a'" None "get"
+                     (Ortac_runtime.report "Array" "make 16 'a'"
+                        (Either.left "Invalid_argument") "get"
                         [("0 <= i < t.size",
                            {
                              Ortac_runtime.start =
@@ -500,7 +501,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     else
                       Some
                         (Ortac_runtime.report "Array" "make 16 'a'"
-                           (Some
+                           (Either.right
                               (Res
                                  (char,
                                    (try
@@ -587,8 +588,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "Array" "make 16 'a'" None
-                           "get"
+                        (Ortac_runtime.report "Array" "make 16 'a'"
+                           (Either.left "Invalid_argument") "get"
                            [("0 <= i < t.size",
                               {
                                 Ortac_runtime.start =
@@ -643,7 +644,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                  then None
                  else
                    Some
-                     (Ortac_runtime.report "Array" "make 16 'a'" None "set"
+                     (Ortac_runtime.report "Array" "make 16 'a'"
+                        (Either.left "Invalid_argument") "set"
                         [("0 <= i < t.size",
                            {
                              Ortac_runtime.start =
@@ -703,8 +705,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "Array" "make 16 'a'" None
-                           "set"
+                        (Ortac_runtime.report "Array" "make 16 'a'"
+                           (Either.left "Invalid_argument") "set"
                            [("0 <= i < t.size",
                               {
                                 Ortac_runtime.start =
@@ -753,8 +755,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                     then None
                     else
                       Some
-                        (Ortac_runtime.report "Array" "make 16 'a'" None
-                           "fill"
+                        (Ortac_runtime.report "Array" "make 16 'a'"
+                           (Either.left "Invalid_argument") "fill"
                            [("0 <= i",
                               {
                                 Ortac_runtime.start =
@@ -802,8 +804,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                        then None
                        else
                          Some
-                           (Ortac_runtime.report "Array" "make 16 'a'" None
-                              "fill"
+                           (Ortac_runtime.report "Array" "make 16 'a'"
+                              (Either.left "Invalid_argument") "fill"
                               [("0 <= j",
                                  {
                                    Ortac_runtime.start =
@@ -854,8 +856,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                        then None
                        else
                          Some
-                           (Ortac_runtime.report "Array" "make 16 'a'" None
-                              "fill"
+                           (Ortac_runtime.report "Array" "make 16 'a'"
+                              (Either.left "Invalid_argument") "fill"
                               [("i + j <= t.size",
                                  {
                                    Ortac_runtime.start =
@@ -909,8 +911,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                        then None
                        else
                          Some
-                           (Ortac_runtime.report "Array" "make 16 'a'" None
-                              "fill"
+                           (Ortac_runtime.report "Array" "make 16 'a'"
+                              (Either.left "Invalid_argument") "fill"
                               [("0 <= i",
                                  {
                                    Ortac_runtime.start =
@@ -959,7 +961,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                           else
                             Some
                               (Ortac_runtime.report "Array" "make 16 'a'"
-                                 None "fill"
+                                 (Either.left "Invalid_argument") "fill"
                                  [("0 <= j",
                                     {
                                       Ortac_runtime.start =
@@ -1012,7 +1014,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                           else
                             Some
                               (Ortac_runtime.report "Array" "make 16 'a'"
-                                 None "fill"
+                                 (Either.left "Invalid_argument") "fill"
                                  [("i + j <= t.size",
                                     {
                                       Ortac_runtime.start =
@@ -1058,7 +1060,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
           else
             Some
               (Ortac_runtime.report "Array" "make 16 'a'"
-                 (Some
+                 (Either.right
                     (Res
                        ((list char),
                          (try (Lazy.force new_state__011_).contents
@@ -1131,7 +1133,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
           else
             Some
               (Ortac_runtime.report "Array" "make 16 'a'"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "mem"
+                 (Either.right (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 7923257a..ff4acf16 100644
--- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
@@ -200,7 +200,7 @@ let ortac_postcond cmd__006_ state__007_ res__008_ =
                  else
                    Some
                      (Ortac_runtime.report "Conjunctive_clauses"
-                        "make 42 'a'" None "set"
+                        "make 42 'a'" (Either.left "Invalid_argument") "set"
                         [("0 <= i < List.length t.contents",
                            {
                              Ortac_runtime.start =
@@ -261,7 +261,8 @@ let ortac_postcond cmd__006_ state__007_ res__008_ =
                     else
                       Some
                         (Ortac_runtime.report "Conjunctive_clauses"
-                           "make 42 'a'" None "set"
+                           "make 42 'a'" (Either.left "Invalid_argument")
+                           "set"
                            [("0 <= i < List.length t.contents",
                               {
                                 Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
index 2732c76d..60428e59 100644
--- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
@@ -322,7 +322,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                else
                  Some
                    (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
-                      (Some (Res (Ortac_runtime.dummy, ()))) "find"
+                      (Either.right (Res (Ortac_runtime.dummy, ()))) "find"
                       [("List.mem (a, b) h.contents",
                          {
                            Ortac_runtime.start =
@@ -373,7 +373,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                else
                  Some
                    (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
-                      None "find"
+                      (Either.left "Not_found") "find"
                       [("not (List.mem a (List.map fst h.contents))",
                          {
                            Ortac_runtime.start =
@@ -437,7 +437,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           else
             Some
               (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "find_opt"
+                 (Either.right (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 =
@@ -488,7 +488,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           else
             Some
               (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "find_all"
+                 (Either.right (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 =
@@ -539,7 +539,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           else
             Some
               (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "mem"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "mem"
                  [("b = List.mem a (List.map fst h.contents)",
                     {
                       Ortac_runtime.start =
@@ -590,7 +590,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           else
             Some
               (Ortac_runtime.report "Hashtbl" "create ~random:false 16"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "length"
+                 (Either.right (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 21b544cf..2bdd2fa2 100644
--- a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml
@@ -150,7 +150,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           else
             Some
               (Ortac_runtime.report "Invariants" "create 42"
-                 (Some (Res (unit, ()))) "push"
+                 (Either.right (Res (unit, ()))) "push"
                  [("List.length x.contents > 0",
                     {
                       Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/record_stm_tests.expected.ml b/plugins/qcheck-stm/test/record_stm_tests.expected.ml
index 56839571..7b813cc8 100644
--- a/plugins/qcheck-stm/test/record_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/record_stm_tests.expected.ml
@@ -115,7 +115,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
              else
                Some
                  (Ortac_runtime.report "Record" "make 42"
-                    (Some (Res (Ortac_runtime.dummy, ()))) "get"
+                    (Either.right (Res (Ortac_runtime.dummy, ()))) "get"
                     [("i = r.value",
                        {
                          Ortac_runtime.start =
@@ -166,7 +166,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                 else
                   Some
                     (Ortac_runtime.report "Record" "make 42"
-                       (Some (Res (Ortac_runtime.dummy, ()))) "get"
+                       (Either.right (Res (Ortac_runtime.dummy, ()))) "get"
                        [("plus1 i = i + 1",
                           {
                             Ortac_runtime.start =
@@ -215,7 +215,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
                 else
                   Some
                     (Ortac_runtime.report "Record" "make 42"
-                       (Some (Res (Ortac_runtime.dummy, ()))) "get"
+                       (Either.right (Res (Ortac_runtime.dummy, ()))) "get"
                        [("plus2 i = i + 2",
                           {
                             Ortac_runtime.start =
diff --git a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
index 67427a8a..bd2d0d37 100644
--- a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
@@ -89,7 +89,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
           else
             Some
               (Ortac_runtime.report "Ref" "make 42"
-                 (Some (Res (Ortac_runtime.dummy, ()))) "get"
+                 (Either.right (Res (Ortac_runtime.dummy, ()))) "get"
                  [("i = r.value",
                     {
                       Ortac_runtime.start =