Fix a bug due to issues with balance

mythril/laser/ethereum/state/world_state.py

@@ -181,7 +181,8 @@ def create_account(
         if code:
             new_account.code = code
         new_account.nonce = nonce
-        new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
+        if balance is not None:
+            new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
 
         self.put_account(new_account)
         return new_account

mythril/laser/ethereum/transaction/transaction_models.py

@@ -225,8 +225,9 @@ def __init__(
         contract_address = (
             contract_address if isinstance(contract_address, int) else None
         )
+        # Balance set to None to allow for pre-existing ether.
         callee_account = world_state.create_account(
-            0, concrete_storage=True, creator=caller.value, address=contract_address
+            None, concrete_storage=True, creator=caller.value, address=contract_address
         )
         callee_account.contract_name = contract_name or callee_account.contract_name
         # init_call_data "should" be false, but it is easier to model the calldata symbolically

mythril/laser/smt/solver/solver.py

@@ -28,6 +28,15 @@ def set_timeout(self, timeout: int) -> None:
         """
         self.raw.set(timeout=timeout)
 
+    def set_unsat_core(self) -> None:
+        """
+        Enables the generation of unsatisfiable cores in the solver. This option must be activated
+        if you intend to identify and extract the minimal set of conflicting constraints that make
+        a problem unsolvable. Useful for diagnosing and debugging unsatisfiable conditions within
+        constraint sets.
+        """
+        self.raw.set(unsat_core=True)
+
     def add(self, *constraints: Bool) -> None:
         """Adds the constraints to this solver.
 
@@ -39,6 +48,17 @@ def add(self, *constraints: Bool) -> None:
         ]
         self.raw.add(z3_constraints)
 
+    def assert_and_track(self, constraints: Bool, name: str) -> None:
+        """
+        Adds a constraint to the solver with an associated name, allowing the constraint to be tracked.
+        This is particularly useful for identifying specific constraints contributing to an unsat.
+
+        :param constraints: The constraints.
+        :param name: A unique identifier for the constraint, used for tracking purposes in unsat core extraction.
+        :return: None
+        """
+        self.raw.assert_and_track(constraints.raw, name)
+
     def append(self, *constraints: Bool) -> None:
         """Adds the constraints to this solver.