fixed inequality checkDisequalities inefficiency
reverted the core solver to do static slicing, added option --bv-core-solver