Skip to content

Commit

Permalink
Merge pull request kind2-mc#1081 from daniel-larraz/ic3ia-gen-prop
Browse files Browse the repository at this point in the history
Slice in IC3IA only if generated property was in input system
  • Loading branch information
daniel-larraz authored Jul 29, 2024
2 parents 4ae2f20 + aaeebd6 commit 576b261
Showing 1 changed file with 8 additions and 3 deletions.
11 changes: 8 additions & 3 deletions src/ic3ia/IC3IA.ml
Original file line number Diff line number Diff line change
Expand Up @@ -940,11 +940,16 @@ let main fwd slice_to_prop prop in_sys param sys =

let sys =
if slice_to_prop then (
(* Only slice if the property does not contain instantiated variables *)
(* The current slicing procedure works on the input system, not the transition system *)
(* Only slice if the property was already present in the original input system.
The current slicing procedure works on the input system, not the transition system *)
match prop.Property.prop_source with
| Assumption _ -> sys (* An instantiated var is also involved, local sofar var *)
| Instantiated _ -> sys
(* Instantiated properties are only included in the transition system *)
| Assumption _ -> sys
(* An instantiated var, local sofar var, is involved. *)
| Generated (None, _) -> sys
(* Currently, only generated properties with an associated position were already
present in the original input system *)
| _ -> fst (InputSystem.trans_sys_of_analysis ~slice_to_prop:prop in_sys param)
)
else sys
Expand Down

0 comments on commit 576b261

Please sign in to comment.