Print object information on Z3TypeError (WIP)

ref #776
AdaCore · Oct 12, 2022 · cb02d27 · cb02d27
1 parent cac97e9
commit cb02d27
Showing 1 changed file with 3 additions and 1 deletion.
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)}"
+            )
         return left < right