Reentrancy vulnerabilities are a critical security risk in smart contracts, posing a significant threat to the entire blockchain ecosystem. These vulnerabilities arise when a malicious attacker exploits the design of a smart contract to execute a function multiple times within a single transaction, potentially draining its funds or manipulating its state in unintended ways. While multiple countermeasures have been proposed to fortify smart contracts against re-entrancy based attacks, automatically verifying their effectiveness remains a difficult problem due to the inherent complexity of smart contracts and evolving attack techniques. In this work, we propose RAVEN:Reentrancy Analysis for Vulnerability Elimination, a sound and precise approach to automatically verify smart contract safety against re-entrancy attacks. At its core, RAVEN performs a content-sensitive semantic relational flow analysis using the polyhedral abstract domain to check hyper-properties like absorption and commutativity of different program segments, which are sufficient to ensure safety against re-entrancy. We have assessed the scalability and precision of RAVEN on real-world smart contracts written in the Solidity programming language. Our findings demonstrate that RAVEN is significantly more effective than previous approaches, in terms of both precision and verification time.