Reentrancy remains one of the most critical and persistent vulnerabilities in Ethereum smart contracts. It allows an attacker to make recursive calls to sensitive functions before the contract’s internal state is properly updated, potentially leading to severe consequences such as unauthorized fund withdrawals. While many tools have been developed to detect or mitigate this issue, a systematic modeling of the input conditions that trigger reentrancy remains underexplored. In this paper, we introduce a novel approach for formally modeling the input patterns responsible for reentrancy scenarios, considering state variables, external call dependencies, and execution sequences. Our method leverages symbolic artificial intelligence techniques to abstract and analyze these inputs, enabling the automatic generation of relevant test cases that simulate realistic attack paths.