From e0995cb94941c09c59619a4448249556c6c04eef Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 5 Dec 2018 10:17:19 +0100
Subject: [PATCH] add equality operations

---
 mythril/laser/ethereum/instructions.py |  1 +
 mythril/laser/smt/bitvec.py            | 24 ++++++++++++++++++++++++
 mythril/laser/smt/bool.py              |  9 +++++++++
 3 files changed, 34 insertions(+)
 create mode 100644 mythril/laser/smt/bool.py

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 64e27dcd..98114143 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -49,6 +49,7 @@ from mythril.laser.ethereum.transaction import (
     TransactionStartSignal,
     ContractCreationTransaction,
 )
+
 from mythril.support.loader import DynLoader
 from mythril.analysis.solver import get_model
 
diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py
index 9a78374b..7290a740 100644
--- a/mythril/laser/smt/bitvec.py
+++ b/mythril/laser/smt/bitvec.py
@@ -1,7 +1,9 @@
 import z3
 
 from mythril.laser.smt.expression import Expression
+from mythril.laser.smt.bool import Bool
 
+# fmt: off
 
 class BitVec(Expression):
     def __init__(self, raw, annotations=None):
@@ -35,6 +37,28 @@ class BitVec(Expression):
         union = self.annotations + other.annotations
         return BitVec(self.raw ^ other.raw, annotations=union)
 
+    def __lt__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return Bool(self.raw < other.raw, annotations=union)
+
+    def __gt__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return Bool(self.raw < other.raw, annotations=union)
+
+    def __eq__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return Bool(self.raw == other.raw, annotations=union)
+
+
+def UGT(a, b):
+    annotations = a.annotations + b.annotations
+    Bool(z3.UGT(a, b), annotations)
+
+
+def ULT(a, b):
+    annotations = a.annotations + b.annotations
+    Bool(z3.ULT(a, b), annotations)
+
 
 def Concat(*args):
     nraw = z3.Concat([a.raw for a in args])
diff --git a/mythril/laser/smt/bool.py b/mythril/laser/smt/bool.py
new file mode 100644
index 00000000..6491e37a
--- /dev/null
+++ b/mythril/laser/smt/bool.py
@@ -0,0 +1,9 @@
+import z3
+
+from mythril.laser.smt.expression import Expression
+
+# fmt: off
+
+
+class Bool(Expression):
+    pass