From 61ee0707aec517489c0251fa8895724323aabbe0 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Fri, 14 Jun 2024 11:49:25 -0500
Subject: [PATCH] Fixes for commit 1cbc4d1

---
 src/kEvent.ml   | 30 +++++++++++++++---------------
 src/transSys.ml |  9 ++++++---
 2 files changed, 21 insertions(+), 18 deletions(-)

diff --git a/src/kEvent.ml b/src/kEvent.ml
index 4fc0f4752..4c2c16c54 100644
--- a/src/kEvent.ml
+++ b/src/kEvent.ml
@@ -307,12 +307,12 @@ let tag_pt level tag str =
 
 (* Output proved property as plain text *)
 let proved_pt mdl level trans_sys k prop = 
+
+  let property = TransSys.property_of_name trans_sys prop in
   (* Only output if status was unknown *)
   if 
-    not (Property.prop_status_known (TransSys.get_prop_status trans_sys prop))
+    not (Property.prop_status_known (Property.get_prop_status property))
   then (
-
-    let property = TransSys.property_of_name trans_sys prop in
     let prop_type = match property.prop_source with 
       | Candidate None -> "Candidate property"
       | Candidate Some (Generated _) -> "Generated candidate property"
@@ -2229,7 +2229,7 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
     (* Property found true for k steps *)
     | (m, PropStatus (p, (Property.PropKTrue k as s))) :: tl -> (
 
-      try
+      try (
         (* Change property status in transition system *)
         TransSys.set_prop_ktrue trans_sys k p;
 
@@ -2239,7 +2239,7 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
           invars
           ((m, (p, s)) :: prop_status)
           tl
-
+      )
       with TransSys.PropertyNotFound _->
         (* Continue without changes *)
         update_trans_sys' trans_sys invars prop_status tl
@@ -2247,13 +2247,13 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
     (* Property found invariant *)
     | (m, PropStatus (p, (Property.PropInvariant cert as s))) :: tl -> (
 
-      try
-        (* Change property status (of all instances with name [p]) *)
-        TransSys.set_prop_invariant trans_sys p cert;
-
+      try (
         (* Output proved property *)
         log_proved m L_warn trans_sys None p;
 
+        (* Change property status (of all instances with name [p]) *)
+        TransSys.set_prop_invariant trans_sys p cert;
+
         let term =
           TransSys.props_list_of_bound trans_sys Numeral.zero
           |> List.assoc p
@@ -2292,7 +2292,7 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
           invars
           ( (m, (p, s)) :: prop_status )
           tl
-
+      )
       with TransSys.PropertyNotFound _->
         (* Continue without changes *)
         update_trans_sys' trans_sys invars prop_status tl
@@ -2300,20 +2300,20 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
     (* Property found false *)
     | (m, PropStatus (p, (Property.PropFalse cex as s))) :: tl -> (
 
-      try
-        (* Change property status in transition system *)
-        TransSys.set_prop_false trans_sys p cex;
-
+      try (
         (* Output disproved property *)
         log_cex true m L_warn input_sys analysis trans_sys p cex ;
 
+        (* Change property status in transition system *)
+        TransSys.set_prop_false trans_sys p cex;
+
         (* Continue with property status added to accumulator *)
         update_trans_sys'
           trans_sys
           invars
           ((m, (p, s)) :: prop_status)
           tl
-
+      )
       with TransSys.PropertyNotFound _->
         (* Continue without changes *)
         update_trans_sys' trans_sys invars prop_status tl
diff --git a/src/transSys.ml b/src/transSys.ml
index c0d56306d..2104d16a9 100644
--- a/src/transSys.ml
+++ b/src/transSys.ml
@@ -1338,9 +1338,12 @@ let init_define_fun_declare_vars_of_bounds t define declare lbound ubound =
 let property_of_name t name =
 
   (* Return the first property with the given name *)
-  List.find
-    (fun { P.prop_name } -> prop_name = name )
-    t.properties
+  try
+    List.find
+      (fun { P.prop_name } -> prop_name = name )
+      t.properties
+  with Not_found ->
+    raise (PropertyNotFound name)
 
 
 (* Get term of property by name *)