Completeness Refinement in Abstract Symbolic Trajectory Evaluation