Bidirectional Symbolic Analysis for Effective Branch Testing