diff --git a/pyproject.toml b/pyproject.toml
index b4a06b30..71e2494d 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -18,7 +18,7 @@ skip_gitignore = true
 
 [tool.poetry]
 name = "horus-compile"
-version = "0.0.6.6"
+version = "0.0.6.7"
 authors = ["Nethermind <hello@nethermind.io>"]
 description = "Use formally verified annotations in your Cairo code"
 classifiers = [
diff --git a/src/horus/__init__.py b/src/horus/__init__.py
index d6ac0959..dbef3514 100644
--- a/src/horus/__init__.py
+++ b/src/horus/__init__.py
@@ -1 +1 @@
-__version__ = "0.0.6.6"
+__version__ = "0.0.6.7"
diff --git a/src/horus/compiler/code_elements.py b/src/horus/compiler/code_elements.py
index c2c1c5b1..c2ced444 100644
--- a/src/horus/compiler/code_elements.py
+++ b/src/horus/compiler/code_elements.py
@@ -64,6 +64,7 @@ class BoolExprCompare(BoolFormula):
     a: Expression
     b: Expression
     comp: str
+    location: Optional[Location] = LocationField
 
     def get_children(self) -> Sequence[Optional["AstNode"]]:
         return [self.a, self.b]
diff --git a/src/horus/compiler/parser_transformer.py b/src/horus/compiler/parser_transformer.py
index a9e2b7fe..037c4445 100644
--- a/src/horus/compiler/parser_transformer.py
+++ b/src/horus/compiler/parser_transformer.py
@@ -131,21 +131,21 @@ def bool_expr_false(self):
     def bool_atom(self, expr):
         return BoolExprAtom(expr)
 
-    @lark.v_args(inline=True)
-    def bool_expr_le(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, "<=")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_le(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, "<=", location=self.meta2loc(meta))
 
-    @lark.v_args(inline=True)
-    def bool_expr_lt(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, "<")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_lt(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, "<", location=self.meta2loc(meta))
 
-    @lark.v_args(inline=True)
-    def bool_expr_ge(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, ">=")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_ge(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, ">=", location=self.meta2loc(meta))
 
-    @lark.v_args(inline=True)
-    def bool_expr_gt(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, ">")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_gt(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, ">", location=self.meta2loc(meta))
 
     @lark.v_args(inline=True)
     def bool_expr_parentheses(self, formula):
diff --git a/src/horus/compiler/z3_transformer.py b/src/horus/compiler/z3_transformer.py
index d98885f1..0e336702 100644
--- a/src/horus/compiler/z3_transformer.py
+++ b/src/horus/compiler/z3_transformer.py
@@ -51,6 +51,7 @@
 )
 from starkware.cairo.lang.compiler.resolve_search_result import resolve_search_result
 from starkware.cairo.lang.compiler.scoped_name import ScopedName
+from starkware.cairo.lang.compiler.type_casts import CairoTypeError
 from starkware.cairo.lang.compiler.type_system_visitor import *
 from starkware.cairo.lang.compiler.type_system_visitor import simplify_type_system
 
@@ -411,7 +412,12 @@ def visit_BoolEqExpr(self, bool_expr: BoolEqExpr):
             self.storage_vars,
             self.is_post,
         )
-        assert a_type == b_type, "Types of lhs and rhs must coincide"
+
+        if a_type != b_type:
+            raise CairoTypeError(
+                f"Types of lhs and rhs must coincide. Got {a_type.format()} and {b_type.format()}",
+                bool_expr.location,
+            )
 
         if isinstance(a_type, TypeStruct):
             result = self.make_struct_eq(bool_expr.a, bool_expr.b, a_type)
@@ -443,7 +449,11 @@ def visit_BoolExprCompare(self, formula: BoolExprCompare):
             self.is_post,
         )
 
-        assert a_type == b_type, "Types of lhs and rhs must coincide"
+        if a_type != b_type:
+            raise CairoTypeError(
+                f"Types of lhs and rhs must coincide. Got {a_type.format()} and {b_type.format()}",
+                formula.location,
+            )
 
         if isinstance(a_type, (TypeFelt, TypePointer)):
             a = self.z3_expression_transformer.visit(a)
@@ -457,6 +467,11 @@ def visit_BoolExprCompare(self, formula: BoolExprCompare):
                 return a >= b
             elif formula.comp == ">":
                 return a > b
+        else:
+            raise CairoTypeError(
+                f"Cannot compare values of type {a_type.format()}",
+                location=formula.location,
+            )
 
     def visit_BoolConst(self, formula: BoolConst):
         return z3.BoolVal(formula.const)