diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index c645b146..e5bdfec4 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -3,7 +3,7 @@ from itertools import product from typing import Optional, Union, cast, Callable, List import z3 -from mythril.laser.smt.bitvec import BitVec, Annotations +from mythril.laser.smt.bitvec import BitVec, Annotations, _padded_operation from mythril.laser.smt.bool import Or, Bool, And @@ -109,7 +109,10 @@ def _comparison_helper( ) return And( - Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union), + Bool( + cast(z3.BoolRef, _padded_operation(a.raw, b.raw, operation)), + annotations=union, + ), Bool(condition) if b.nested_functions else Bool(True), a.input_ == b.input_ if inputs_equal else a.input_ != b.input_, )