Fix quantifier instantiation bug in cbqi, add default priorities in rewrite engine.