From 94cd6364b08bbabb9a24e52ea9bbfeeb1a134898 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 7 Oct 2019 15:32:41 +0100 Subject: [PATCH] Use padded operation over operation (#1229) * Use padded operation over operation * Add missing operation --- mythril/laser/smt/bitvecfunc.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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_, )