// This rule uses forall, with it, all control flows must match.
// The exists4.c was extended to add a c() in comparison to exists2.c
// this is done to show that using forall will still have an effect
// on bar() even though it does not match on main()
// This is the default behaviour when + or - is used as well.