diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index da70f2be..7ca8b4df 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -553,7 +553,7 @@ class Instruction: + str(hash(simplify(exponent))) + ")", 256, - base.annotations + exponent.annotations, + base.annotations.union(exponent.annotations), ) ) # Hash is used because str(symbol) takes a long time to be converted to a string else: @@ -925,7 +925,7 @@ class Instruction: if data.symbolic: - annotations = set() + annotations = set() # Type: Set for b in state.memory[index : index + length]: if isinstance(b, BitVec): diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 5a3f1ca1..407f6565 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -22,11 +22,11 @@ from mythril.laser.smt.array import K, Array, BaseArray from mythril.laser.smt.solver import Solver, Optimize, SolverStatistics from mythril.laser.smt.model import Model -from typing import Union, Any, Optional, List, TypeVar, Generic +from typing import Union, Any, Optional, Set, TypeVar, Generic import z3 -Annotations = Optional[List[Any]] +Annotations = Optional[Set[Any]] T = TypeVar("T", bound=Union[bool.Bool, z3.BoolRef]) U = TypeVar("U", bound=Union[BitVec, z3.BitVecRef])