Motivated by the immutable nature of Ethereum smart contracts and of their\ntransactions, quite many approaches have been proposed to detect defects and\nsecurity problems before smart contracts become persistent in the blockchain\nand they are granted control on substantial financial value.\n Because smart contracts source code might not be available, static analysis\napproaches mostly face the challenge of analysing compiled Ethereum bytecode,\nthat is available directly from the official blockchain. However, due to the\nintrinsic complexity of Ethereum bytecode (especially in jump resolution),\nstatic analysis encounters significant obstacles that reduce the accuracy of\nexiting automated tools.\n This paper presents a novel static analysis algorithm based on the symbolic\nexecution of the Ethereum operand stack that allows us to resolve jumps in\nEthereum bytecode and to construct an accurate control-flow graph (CFG) of the\ncompiled smart contracts. EtherSolve is a prototype implementation of our\napproach. Experimental results on a significant set of real world Ethereum\nsmart contracts show that EtherSolve improves the accuracy of the execrated\nCFGs with respect to the state of the art available approaches.\n Many static analysis techniques are based on the CFG representation of the\ncode and would therefore benefit from the accurate extraction of the CFG. For\nexample, we implemented a simple extension of EtherSolve that allows to detect\ninstances of the re-entrancy vulnerability.\n