mu bool Reachable(
 Module  s_mod,
 PrCount s_pc,
 Local   s_CL,
 Global  s_CG,
 Local   s_ENTRY_CL,
 Global  s_ENTRY_CG
)
s_mod <  s_pc,
s_pc  <  s_CL,
s_CL  ~+ s_ENTRY_CL,
s_CL  <  s_CG,
s_CG  ~+ s_ENTRY_CG
(
  false

  // early termination
  | ( exists Module  t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global  t_ENTRY_CG.
        (    target(t_mod,t_pc) &
             Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG)
    )   )

|(enforce(s_mod, s_CL, s_CG)  &

    (
    // initial conf
    (s_mod=0 & s_pc=0 )


    // forward propagation on call transitions
    | (        s_pc=0 & CopyLocals(s_mod,s_ENTRY_CL,s_CL)
             & (exists Module t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global t_ENTRY_CG.
                              (   (Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG) & CopyGlobals(s_mod,t_CG,s_CG) )
                                      & CopyGlobals(s_mod, t_CG, s_ENTRY_CG)
                                      & programCall(t_mod,s_mod,t_pc,t_CL,s_CL,t_CG)
      )         )              )


    // forward propagation on internal transitions on current set (not just the frontier from prev round)
    | (exists PrCount t_pc, Local t_CL, Global t_CG.
            (    (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
                 &(
                    ( programInt1(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
                      & CopyVariables_ProgramInt(s_mod,t_pc,t_CL,s_CL,t_CG,s_CG)
                    )
                    | programInt3(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
      )     )     )

    | (exists PrCount t_pc.
         (  (Reachable(s_mod,t_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
            & programInt2(s_mod,t_pc,s_pc,s_CL,s_CG)
      )  )


    // forward propagation on SkipCall (jump from exit to return)
    | (exists PrCount t_pc, Global t_CG, Module u_mod, PrCount u_pc, Local u_ENTRY_CL.
           ( exists  Local t_CL.
            (  (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG)  // t is reachable
              & SkipCall(s_mod,t_pc,s_pc))
              & programCall(s_mod,u_mod,t_pc,t_CL,u_ENTRY_CL,t_CG)
              & SetReturnTS(s_mod,u_mod,t_pc,u_pc,t_CL,s_CL,t_CG,s_CG)
           ))
         &
         ( exists Local u_CL, Global u_CG.
            (
                (Reachable(u_mod,u_pc,u_CL,u_CG,u_ENTRY_CL,t_CG)        // u is reachable
              & Exit(u_mod,u_pc))                                       // u is an exit
              & SetReturnUS(s_mod,u_mod,t_pc,u_pc,u_CL,s_CL,u_CG,s_CG)
      )  )  )

  )
 )
);

/******************************************************************************************************/
//                                Reachability formula                                            *
/******************************************************************************************************/

(  exists Module  s_mod, PrCount s_pc, Local s_CL, Global s_CG, Local s_ENTRY_CL, Global s_ENTRY_CG.
        (    target(s_mod,s_pc) &
             Reachable(s_mod,s_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG)
        )
);