Merge pull request #1076 from daniel-larraz/fix-1cbc4d1

Fixes for commit 1cbc4d1
kind2-mc · Jun 14, 2024 · b17c15a · b17c15a
2 parents f512d2e + 61ee070
commit b17c15a
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 18 deletions.
diff --git 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,21 +2239,21 @@ 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
     )
     (* 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,28 +2292,28 @@ 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
     )
     (* 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
@@ -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 *)