Symbolic execution PoC

[arcz]

trafficstars

A quick PoC that breaks this contract (included in tests):

contract VulnerableContract {
   function func_one(int256 x) public pure {
     if (x / 4 == -20) {
       assert(false); // BUG
     }
   }

   function func_two(int128 x) public payable {
     if ((msg.value >> 30) / 7 == 2) {
       assert(false); // BUG
     }
   }
}

Non-nix tests fail because I need to figure out how to install solvers :p