From 4b1d1fbbbb6348fefa6771445702ee780c669f99 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 27 Feb 2024 15:59:10 +0100
Subject: [PATCH] Add an assert for exceptional behaviour in scenario

Collect the name of the exception when checking an exceptional
postcondition (not the arguments as they are not always specified).
---
 CHANGES.md                                    |  3 +-
 examples/lwt_dllist_tests.ml                  | 20 +++---
 examples/varray_circular_tests.ml             | 56 ++++++++++-------
 examples/varray_tests.ml                      | 62 ++++++++++---------
 .../src/runtime/ortac_runtime_qcheck_stm.ml   | 10 ++-
 plugins/qcheck-stm/src/stm_of_ir.ml           | 50 +++++++++------
 plugins/qcheck-stm/test/array.ml              |  2 +
 .../test/array_stm_tests.expected.ml          | 55 ++++++++--------
 .../conjunctive_clauses_stm_tests.expected.ml |  9 +--
 .../test/hashtbl_stm_tests.expected.ml        | 15 ++---
 .../test/invariants_stm_tests.expected.ml     |  2 +-
 .../test/record_stm_tests.expected.ml         |  6 +-
 .../qcheck-stm/test/ref_stm_tests.expected.ml |  2 +-
 13 files changed, 168 insertions(+), 124 deletions(-)

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 1fd9e3bb..13148610 100644
--- a/examples/lwt_dllist_tests.ml
+++ b/examples/lwt_dllist_tests.ml
@@ -338,7 +338,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 =
@@ -387,7 +387,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 =
@@ -445,7 +445,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 =
@@ -497,8 +497,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 =
@@ -559,7 +559,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 =
@@ -611,8 +611,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 =
@@ -665,7 +665,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 =
@@ -717,7 +717,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 7dd2b36f..16637e26 100644
--- a/examples/varray_circular_tests.ml
+++ b/examples/varray_circular_tests.ml
@@ -766,7 +766,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 =
@@ -819,7 +820,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 =
@@ -877,7 +878,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 =
@@ -930,7 +932,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 =
@@ -987,7 +989,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 =
@@ -1050,7 +1053,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 =
@@ -1099,7 +1103,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 =
@@ -1155,7 +1160,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 =
@@ -1211,7 +1217,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 =
@@ -1260,7 +1267,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 =
@@ -1318,7 +1326,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 =
@@ -1374,7 +1383,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 =
@@ -1423,7 +1433,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 =
@@ -1479,7 +1489,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 =
@@ -1535,7 +1546,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 =
@@ -1584,7 +1596,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 =
@@ -1641,7 +1653,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 =
@@ -1690,7 +1703,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 =
@@ -1739,7 +1752,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 =
@@ -1803,7 +1816,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 =
@@ -1876,7 +1889,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 8c6b7fbf..d40c5c45 100644
--- a/examples/varray_tests.ml
+++ b/examples/varray_tests.ml
@@ -766,7 +766,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 =
@@ -818,8 +819,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 =
@@ -877,7 +878,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 =
@@ -929,8 +931,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 =
@@ -986,8 +988,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 =
@@ -1048,7 +1050,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 =
@@ -1096,8 +1098,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 =
@@ -1150,7 +1152,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 =
@@ -1204,7 +1207,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 =
@@ -1252,8 +1255,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 =
@@ -1309,7 +1312,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 =
@@ -1363,7 +1366,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 =
@@ -1411,8 +1414,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 =
@@ -1465,7 +1468,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 =
@@ -1519,7 +1523,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 =
@@ -1567,8 +1571,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 =
@@ -1623,7 +1627,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 =
@@ -1672,7 +1676,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 =
@@ -1721,7 +1725,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 =
@@ -1784,8 +1788,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 =
@@ -1856,7 +1860,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 9c69f0bb..23640168 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 ffa9b6a7..64dffbfc 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_mappend = list_fold_expr "++" "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
@@ -305,12 +315,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
@@ -480,13 +485,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
@@ -496,7 +504,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 ] ]);
               ]))
@@ -550,14 +558,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_mappend (postcond @ invariants) |> ok
@@ -582,13 +587,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
@@ -598,7 +605,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.ml b/plugins/qcheck-stm/test/array.ml
index 7313680a..a96b821e 100644
--- a/plugins/qcheck-stm/test/array.ml
+++ b/plugins/qcheck-stm/test/array.ml
@@ -1 +1,3 @@
 include Array
+
+let get a _ = get a 7
diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
index a9b29f24..ed978831 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"
@@ -367,7 +369,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
@@ -446,7 +448,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 =
@@ -499,7 +502,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
@@ -586,8 +589,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 =
@@ -642,7 +645,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 =
@@ -702,8 +706,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,7 +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 =
@@ -799,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 +857,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 =
@@ -906,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 =
@@ -955,8 +960,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 =
@@ -1010,7 +1015,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 +1061,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 +1134,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 18ad38f8..b6e6981a 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 =
@@ -201,7 +201,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 =
@@ -262,7 +262,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 7ca80f09..d01e81ed 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
@@ -325,7 +326,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 =
@@ -376,7 +377,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 =
@@ -440,7 +441,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 =
@@ -491,7 +492,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 =
@@ -542,7 +543,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 =
@@ -593,7 +594,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 0be57055..05ceb2a8 100644
--- a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml
@@ -151,7 +151,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 8cda4a5f..976ba395 100644
--- a/plugins/qcheck-stm/test/record_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/record_stm_tests.expected.ml
@@ -119,7 +119,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 =
@@ -169,7 +169,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 =
@@ -220,7 +220,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 ba6eabcb..af1f4063 100644
--- a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
@@ -90,7 +90,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 =