Don't prune states that are reachable if callvalue > 0

mythril/laser/ethereum/plugins/implementations/mutation_pruner.py

@@ -3,12 +3,14 @@ from mythril.laser.ethereum.plugins.plugin import LaserPlugin
 from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
     MutationAnnotation,
 )
+from mythril.laser.smt.bitvec_helper import UGT
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
-from mythril.laser.smt import And, symbol_factory
+from mythril.analysis import solver
+from mythril.exceptions import UnsatError, CriticalError
 
 
 class MutationPruner(LaserPlugin):
@@ -38,27 +40,23 @@ class MutationPruner(LaserPlugin):
         def sstore_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
 
-        @symbolic_vm.pre_hook("CALL")
-        def call_mutator_hook(global_state: GlobalState):
-            global_state.annotate(MutationAnnotation())
-
-        @symbolic_vm.pre_hook("STATICCALL")
-        def staticcall_mutator_hook(global_state: GlobalState):
-            global_state.annotate(MutationAnnotation())
-
         @symbolic_vm.laser_hook("add_world_state")
         def world_state_filter_hook(global_state: GlobalState):
-            if And(
-                *global_state.world_state.constraints[:]
-                + [
-                    global_state.environment.callvalue
-                    > symbol_factory.BitVecVal(0, 256)
-                ]
-            ).is_false:
-                return
+
             if isinstance(
                 global_state.current_transaction, ContractCreationTransaction
             ):
                 return
+
+            try:
+                constraints = global_state.world_state.constraints + [
+                    global_state.environment.callvalue > 0
+                ]
+
+                solver.get_model(constraints)
+                return
+            except UnsatError:
+                pass
+
             if len(list(global_state.get_annotations(MutationAnnotation))) == 0:
                 raise PluginSkipWorldState