From 0ffe7094292e38c7d0f1fabdd327971e20d5c548 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 8 Jul 2019 11:03:05 +0530 Subject: [PATCH] Handle __eq__ and __ne__ for BitVecs with different sizes --- mythril/laser/smt/bitvec.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index 0928cebf..61747486 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -190,6 +190,8 @@ class BitVec(Expression[z3.BitVecRef]): ) union = self.annotations.union(other.annotations) + if self.raw.size() != other.raw.size(): + return Bool(z3.BoolVal(False), annotations=union) # MYPY: fix complaints due to z3 overriding __eq__ return Bool(cast(z3.BoolRef, self.raw == other.raw), annotations=union) @@ -208,6 +210,8 @@ class BitVec(Expression[z3.BitVecRef]): ) union = self.annotations.union(other.annotations) + if self.raw.size() != other.raw.size(): + return Bool(z3.BoolVal(True), annotations=union) # MYPY: fix complaints due to z3 overriding __eq__ return Bool(cast(z3.BoolRef, self.raw != other.raw), annotations=union)