Skip to content

Commit

Permalink
InvGen: Always start generating invariants from the top
Browse files Browse the repository at this point in the history
  • Loading branch information
daniel-larraz committed Jan 11, 2024
1 parent 6c64112 commit 172b0ef
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/invgen/invGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -722,7 +722,9 @@ module Make (Graph : GraphSig) : Out = struct
)
(* If in modular mode, we already ran on the subsystems.
Might as well start with the current top system since it's new. *)
|> ( if modular then identity else List.rev )
(* Update: If in monolithic mode, also start with the current top system
since it is not clear that starting from the bottom really helps *)
(*|> ( if modular then identity else List.rev )*)
|> function
| [] ->
KEvent.log L_info "%s no candidate to run on" (pref_s two_state) ;
Expand Down

0 comments on commit 172b0ef

Please sign in to comment.