Add origin constraints to suicide & ether_thief mods

mythril/analysis/modules/ether_thief.py

@@ -14,6 +14,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction import ContractCreationTransaction
 
 from mythril.laser.smt import UGT, UGE
+from mythril.laser.smt.bool import And
 
 log = logging.getLogger(__name__)
 
@@ -90,7 +91,9 @@ class EtherThief(DetectionModule):
             This prevents false positives where the owner willingly transfers ownership to another address.
             """
             if not isinstance(tx, ContractCreationTransaction):
-                constraints += [tx.caller != ACTORS.creator]
+                constraints.append(
+                    And(tx.caller == ACTORS.attacker, tx.caller == tx.origin)
+                )
 
         attacker_address_bitvec = ACTORS.attacker
 

mythril/analysis/modules/suicide.py

@@ -5,6 +5,7 @@ from mythril.exceptions import UnsatError
 from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction.symbolic import ACTORS
+from mythril.laser.smt.bool import And
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
@@ -68,7 +69,9 @@ class SuicideModule(DetectionModule):
 
         for tx in state.world_state.transaction_sequence:
             if not isinstance(tx, ContractCreationTransaction):
-                constraints.append(tx.caller == ACTORS.attacker)
+                constraints.append(
+                    And(tx.caller == ACTORS.attacker, tx.caller == tx.origin)
+                )
         try:
             try:
                 transaction_sequence = solver.get_transaction_sequence(