Merge branch 'develop' into fix/memory

.circleci/config.yml

@@ -110,6 +110,7 @@ jobs:
                 --timeout 60 \
                 --output-dir /opt/edelweiss \
                 --s3 \
+                --dynamodb \
                 --circle-ci CircleCI/mythril.csv \
                 --ignore-false-positives $IGNORE_FALSE_POSITIVES \
                 --ignore-regressions $IGNORE_REGRESSIONS

mythril/laser/smt/bitvec.py

@@ -202,6 +202,9 @@ class BitVec(Expression[z3.BitVecRef]):
             )
 
         union = self.annotations.union(other.annotations)
+        # Some of the BitVecs can be 512 bit due to sha3()
+        if self.raw.size() != other.raw.size():
+            return Bool(z3.BoolVal(False), annotations=union)
         # MYPY: fix complaints due to z3 overriding __eq__
         return Bool(cast(z3.BoolRef, self.raw == other.raw), annotations=union)
 
@@ -220,6 +223,9 @@ class BitVec(Expression[z3.BitVecRef]):
             )
 
         union = self.annotations.union(other.annotations)
+        # Some of the BitVecs can be 512 bit due to sha3()
+        if self.raw.size() != other.raw.size():
+            return Bool(z3.BoolVal(True), annotations=union)
         # MYPY: fix complaints due to z3 overriding __eq__
         return Bool(cast(z3.BoolRef, self.raw != other.raw), annotations=union)
 

mythril/mythril/mythril_config.py

@@ -175,7 +175,7 @@ class MythrilConfig:
         :param rpc: either of the strings - ganache, infura-mainnet, infura-rinkeby, infura-kovan, infura-ropsten
         """
         if rpc == "ganache":
-            rpcconfig = ("localhost", 8545, False)
+            rpcconfig = ("localhost", 7545, False)
         else:
             m = re.match(r"infura-(.*)", rpc)
             if m and m.group(1) in ["mainnet", "rinkeby", "kovan", "ropsten"]:

tests/mythril/mythril_config_test.py

@@ -19,7 +19,7 @@ def test_config_path_dynloading():
 
 rpc_types_tests = [
     ("infura", "mainnet.infura.io", 443, True),
-    ("ganache", "localhost", 8545, True),
+    ("ganache", "localhost", 7545, True),
     ("infura-rinkeby", "rinkeby.infura.io", 443, True),
     ("infura-ropsten", "ropsten.infura.io", 443, True),
     ("infura-kovan", "kovan.infura.io", 443, True),