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 b99d41a1..6a244585 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 5ee5ed9d..1d3c3170 100644
--- a/examples/varray_circular_tests.ml
+++ b/examples/varray_circular_tests.ml
@@ -765,7 +765,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 =
@@ -818,7 +819,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 =
@@ -876,7 +877,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 =
@@ -929,7 +931,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 =
@@ -986,7 +988,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 =
@@ -1049,7 +1052,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 =
@@ -1098,7 +1102,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 =
@@ -1154,7 +1159,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 =
@@ -1210,7 +1216,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 =
@@ -1259,7 +1266,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 =
@@ -1317,7 +1325,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 =
@@ -1373,7 +1382,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 =
@@ -1422,7 +1432,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 =
@@ -1478,7 +1488,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 =
@@ -1534,7 +1545,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 =
@@ -1583,7 +1595,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 =
@@ -1640,7 +1652,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 =
@@ -1689,7 +1702,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 =
@@ -1738,7 +1751,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 =
@@ -1802,7 +1815,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 =
@@ -1875,7 +1888,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 1395fbc5..ecc3f479 100644
--- a/examples/varray_tests.ml
+++ b/examples/varray_tests.ml
@@ -765,7 +765,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 =
@@ -817,8 +818,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 =
@@ -876,7 +877,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 =
@@ -928,8 +930,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 =
@@ -985,8 +987,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 =
@@ -1047,7 +1049,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 =
@@ -1095,8 +1097,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 =
@@ -1149,7 +1151,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 =
@@ -1203,7 +1206,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 =
@@ -1251,8 +1254,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 =
@@ -1308,7 +1311,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 =
@@ -1362,7 +1365,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 =
@@ -1410,8 +1413,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 =
@@ -1464,7 +1467,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 =
@@ -1518,7 +1522,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 =
@@ -1566,8 +1570,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 =
@@ -1622,7 +1626,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 =
@@ -1671,7 +1675,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 =
@@ -1720,7 +1724,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 =
@@ -1783,8 +1787,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 =
@@ -1855,7 +1859,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 b60ca23b..111e7c76 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,7 +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);
-                (Nolabel, if normal then ret_val else enone);
+                (Nolabel, ret_val);
                 (Nolabel, cmd);
                 (Nolabel, elist [ pexp_tuple [ term; l ] ]);
               ]))
@@ -540,14 +548,11 @@ 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 ~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
@@ -572,13 +577,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
@@ -588,7 +595,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 505c4166..5f28eb1b 100644
--- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
@@ -18,13 +18,15 @@ module Spec =
       match cmd__001_ with
       | Length -> Format.asprintf "%s %s" "length" "sut"
       | Get i ->
-          Format.asprintf "%s %s %a" "get" "sut" (Util.Pp.pp_int true) i
+          Format.asprintf "protect (fun () -> %s %s %a)" "get" "sut"
+            (Util.Pp.pp_int true) i
       | Set (i_1, a_1) ->
-          Format.asprintf "%s %s %a %a" "set" "sut" (Util.Pp.pp_int true) i_1
-            (Util.Pp.pp_char true) a_1
+          Format.asprintf "protect (fun () -> %s %s %a %a)" "set" "sut"
+            (Util.Pp.pp_int true) i_1 (Util.Pp.pp_char true) a_1
       | Fill (i_2, j, a_2) ->
-          Format.asprintf "%s %s %a %a %a" "fill" "sut" (Util.Pp.pp_int true)
-            i_2 (Util.Pp.pp_int true) j (Util.Pp.pp_char true) a_2
+          Format.asprintf "protect (fun () -> %s %s %a %a %a)" "fill" "sut"
+            (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 %s" "to_list" "sut"
       | Mem a_3 ->
           Format.asprintf "%s %a %s" "mem" (Util.Pp.pp_char true) a_3 "sut"
@@ -366,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
@@ -445,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 =
@@ -498,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
@@ -585,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 =
@@ -641,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 =
@@ -701,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 =
@@ -751,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 =
@@ -800,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 =
@@ -852,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 =
@@ -907,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 =
@@ -957,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 =
@@ -1010,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 =
@@ -1056,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
@@ -1129,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 273163c1..51b843f9 100644
--- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
@@ -37,8 +37,8 @@ module Spec =
     let show_cmd cmd__001_ =
       match cmd__001_ with
       | Set (i_1, a_2) ->
-          Format.asprintf "%s %s %a %a" "set" "sut" (Util.Pp.pp_int true) i_1
-            (Util.Pp.pp_char true) a_2
+          Format.asprintf "protect (fun () -> %s %s %a %a)" "set" "sut"
+            (Util.Pp.pp_int true) i_1 (Util.Pp.pp_char true) a_2
     type nonrec state = {
       contents: char list }
     let init_state =
@@ -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 e0292dd8..a54804c1 100644
--- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
@@ -53,7 +53,8 @@ module Spec =
           Format.asprintf "%s %s %a %a" "add" "sut" (Util.Pp.pp_char true)
             a_2 (Util.Pp.pp_int true) b_2
       | Find a_3 ->
-          Format.asprintf "%s %s %a" "find" "sut" (Util.Pp.pp_char true) a_3
+          Format.asprintf "protect (fun () -> %s %s %a)" "find" "sut"
+            (Util.Pp.pp_char true) a_3
       | Find_opt a_4 ->
           Format.asprintf "%s %s %a" "find_opt" "sut" (Util.Pp.pp_char true)
             a_4
@@ -324,7 +325,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 =
@@ -375,7 +376,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 =
@@ -439,7 +440,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 =
@@ -490,7 +491,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 =
@@ -541,7 +542,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 =
@@ -592,7 +593,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 573741e8..5cae59e5 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 5db0ba73..309588d8 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 ff164cc4..e571bb09 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 =