fix bug of exception

Author: reb-ddm

core/KaSa_rep/frontend/preprocess.ml

@@ -2349,8 +2349,11 @@ let translate_c_compil parameters error handler compil =
         match enriched_rule.Cckappa_sig.e_rule_label with
         | None -> error, rule_label_map
         | Some (label, _) ->
-          Ckappa_sig.Rule_label_map_and_set.Map.add parameters error label
-            rule_id rule_label_map)
+          let error, map =
+            Ckappa_sig.Rule_label_map_and_set.Map.add_or_overwrite parameters
+              error label rule_id rule_label_map
+          in
+          error, map)
       c_rules Ckappa_sig.Rule_label_map_and_set.Map.empty
   in
 

core/KaSa_rep/reachability_analysis/analyzer_headers.ml

@@ -413,20 +413,19 @@ module AbstractWSMap (MapT : Map_wrapper.S_with_logs) = struct
       Ckappa_sig.Views_bdu.build_variables_list parameters bdu_handler error
         working_set_guards
     in
-    let current_working_set = MapT.Map.empty in
     let result, bdu_handler, error =
       MapT.Map.fold
         (fun rule_id mvbdu (current_working_set, bdu_handler, error) ->
           let error, bdu_handler, mvbdu =
             abstract_away_working_set_vars parameters error bdu_handler mvbdu
               working_set_mvbdu working_set_guards_hcons
           in
-          let error, current_working_set =
+          let error', current_working_set =
             MapT.Map.add parameters error rule_id mvbdu current_working_set
           in
           current_working_set, bdu_handler, error)
         dynamic_local
-        (current_working_set, bdu_handler, error)
+        (MapT.Map.empty, bdu_handler, error)
     in
     error, bdu_handler, result
 end

core/KaSa_rep/reachability_analysis/views_domain.ml

@@ -3264,10 +3264,9 @@ module Domain = struct
 
   let print_bdu_update_map_cartesian_abstraction parameters bdu_handler error
       handler_kappa with_threshold =
-    print_bdu_update_map_gen_decomposition ~sort:true
-      ~smash:true ~show_dep_with_dimmension_higher_than:1
-      mvbdu_cartesian_abstraction parameters bdu_handler error handler_kappa
-      with_threshold
+    print_bdu_update_map_gen_decomposition ~sort:true ~smash:true
+      ~show_dep_with_dimmension_higher_than:1 mvbdu_cartesian_abstraction
+      parameters bdu_handler error handler_kappa with_threshold
 
   (*****************************************************************)
   (*Print for relational properties*)