changes on the flow down rule checking: 1) only check a relation bet array and index...

changes on the flow down rule checking: 1) only check a relation bet array and index value when array access node is the LHS of the assignment node. When an array access is RHS, index and array should be independent.
2) have a better way to check implicit flow. after conditional branch, keep conditional location as a constraint location and then check if an assignment located inside the conditional branch block respects this constraint.