add simple loop constraints
add simple loop constraints
add someTermCondOnEachPath support
add assumeImplies support
add support for weak-cf
fix some termcond on each path