diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py
index e8857106..04d2620a 100644
--- a/mythril/laser/smt/__init__.py
+++ b/mythril/laser/smt/__init__.py
@@ -38,6 +38,7 @@ class _SmtSymbolFactory(SymbolFactory):
     An implementation of a SymbolFactory that creates symbols using
     the classes in: mythril.laser.smt
     """
+
     @staticmethod
     def BitVecVal(value: int, size: int, annotations=None):
         """ Creates a new bit vector with a concrete value """
@@ -56,6 +57,7 @@ class _Z3SymbolFactory(SymbolFactory):
     An implementation of a SymbolFactory that directly returns
     z3 symbols
     """
+
     @staticmethod
     def BitVecVal(value: int, size: int, annotations=None):
         """ Creates a new bit vector with a concrete value """
@@ -69,4 +71,3 @@ class _Z3SymbolFactory(SymbolFactory):
 
 # This is the instance that other parts of mythril should use
 symbol_factory = _Z3SymbolFactory()
-
diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py
index 9aa3944f..1bbe5f7b 100644
--- a/mythril/laser/smt/bitvec.py
+++ b/mythril/laser/smt/bitvec.py
@@ -108,4 +108,3 @@ def SRem(a: BitVec, b: BitVec) -> BitVec:
 def UDiv(a: BitVec, b: BitVec) -> BitVec:
     union = a.annotations + b.annotations
     return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)
-
diff --git a/mythril/laser/smt/bool.py b/mythril/laser/smt/bool.py
index 5f72eebf..934c4a9b 100644
--- a/mythril/laser/smt/bool.py
+++ b/mythril/laser/smt/bool.py
@@ -8,10 +8,17 @@ from mythril.laser.smt.expression import Expression
 class Bool(Expression):
 
     @property
-    def is_false(self):
+    def is_false(self) -> bool:
         return z3.is_false(self.raw)
 
     @property
-    def is_true(self):
+    def is_true(self) -> bool:
         return z3.is_true(self.raw)
 
+
+def is_false(a: Bool) -> bool:
+    return is_false(a)
+
+
+def is_true(a: Bool) -> bool:
+    return is_true(a)