fix broken edge case where sign_bit_set is symbolic

mythril/laser/ethereum/instructions.py

@@ -651,10 +651,21 @@ class Instruction:
 
         if s0 <= 31:
             testbit = s0 * 8 + 7
-            if not is_true(simplify((s1 & (1 << testbit)) == 0)):
+            sign_bit_set = simplify((s1 & (1 << testbit)) == 1)
+            if is_true(sign_bit_set):
                 mstate.stack.append(s1 | (TT256 - (1 << testbit)))
-            else:
+            elif is_false(sign_bit_set):
                 mstate.stack.append(s1 & ((1 << testbit) - 1))
+            else:
+                mstate.stack.append(
+                    simplify(
+                        If(
+                            sign_bit_set,
+                            s1 | (TT256 - (1 << testbit)),
+                            s1 & ((1 << testbit) - 1),
+                        )
+                    )
+                )
         else:
             mstate.stack.append(s1)
 

requirements.txt

@@ -4,13 +4,12 @@ coverage
 py_ecc==1.6.0
 eth_abi==1.3.0
 eth-account>=0.1.0a2,<=0.3.0
-ethereum>=2.3.2
+ethereum==2.3.1
 ethereum-input-decoder>=0.2.2
 eth-hash>=0.1.0
 eth-keyfile>=0.5.1
 eth-keys>=0.2.0b3,<0.3.0
 eth-rlp>=0.1.0
-eth-tester==0.1.0b32
 eth-typing>=2.0.0
 eth-utils==1.9.0
 jinja2>=2.9
@@ -19,7 +18,6 @@ numpy==1.19.0
 persistent>=4.2.0
 plyvel
 py-flags
-py-evm==0.3.0a13
 py-solc-x==1.0.0
 py-solc
 pytest>=3.6.0