New model-based array procedure
Updates to model-based array solver
Minor fixes to bv and theory_engine
Added assertion