search

pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
996 stars 47 forks source link

z3 boolean isn't number-comparable #283

Open pschanely opened 1 month ago

pschanely commented 1 month ago 
          [from `test_assume_has_status_reason`:](https://github.com/HypothesisWorks/hypothesis/actions/runs/10046646626/job/27766587120?pr=4034#step:6:3400)
Traceback (most recent call last):
  File ".../crosshair/libimpl/builtinslib.py", line 900, in __abs__
    return self._unary_op(lambda v: z3.If(v < 0, -v, v))
  File ".../crosshair/libimpl/builtinslib.py", line 319, in _unary_op
    return self.__class__(op(self.var), self.python_type)
  File ".../crosshair/libimpl/builtinslib.py", line 900, in <lambda>
    return self._unary_op(lambda v: z3.If(v < 0, -v, v))
TypeError: '<' not supported between instances of 'BoolRef' and 'int'

whereas in Python issubclass(bool, int) and so you can indeed compare them.

Originally posted by @Zac-HD in https://github.com/HypothesisWorks/hypothesis/issues/4034#issuecomment-2243950206