Print object information on Z3TypeError (WIP)

ref #776
AdaCore · Oct 14, 2022 · b1df95b · b1df95b
1 parent e91b737
commit b1df95b
Showing 1 changed file with 9 additions and 3 deletions.
diff --git a/rflx/expression.py b/rflx/expression.py
@@ -1947,7 +1947,9 @@ def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
         if not isinstance(left, z3.ArithRef) or not isinstance(right, z3.ArithRef):
-            raise Z3TypeError("less relation between non-arithmetic terms")
+            raise Z3TypeError(
+                f"less relation between non-arithmetic terms: {repr(left)} - {repr(right)}, {str(left)} - {str(right)}, {type(left)} - {type(right)}; {repr(self.left)} - {repr(self.right)}; {repr(self.left.type_)} - {repr(self.right.type_)}; {type(self.left.z3expr())} - {type(self.right.z3expr())}"
+            )
         return left < right
 
 
@@ -2031,7 +2033,9 @@ def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
         if not isinstance(left, z3.ArithRef) or not isinstance(right, z3.ArithRef):
-            raise Z3TypeError("greater-equal relation between non-arithmetic terms")
+            raise Z3TypeError(
+                f"less relation between non-arithmetic terms: {repr(left)} - {repr(right)}, {str(left)} - {str(right)}, {type(left)} - {type(right)}"
+            )
         return left >= right
 
 
@@ -2060,7 +2064,9 @@ def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
         if not isinstance(left, z3.ArithRef) or not isinstance(right, z3.ArithRef):
-            raise Z3TypeError("greater relation between non-arithmetic terms")
+            raise Z3TypeError(
+                f"less relation between non-arithmetic terms: {repr(left)} - {repr(right)}, {str(left)} - {str(right)}, {type(left)} - {type(right)}"
+            )
         return left > right