fix for nonterminating model-based array loop
BV strategy for SMT-EVAL