`z3.z3types.Z3Exception: b'parser error'` from interaction with `TypeVar`

[Zac-HD]

repro extracted from this test, in https://github.com/HypothesisWorks/hypothesis/pull/4034:

import typing
from hypothesis import given, settings
T = typing.TypeVar("T")

@settings(backend="crosshair")
@given(...)
def test_typevar_type_is_consistent(a: T, b: T):
    a != b

  File "repro.py", line 8, in test_typevar_type_is_consistent
    a != b
  File ".../crosshair/libimpl/builtinslib.py", line 381, in __ne__
    coerced = type(self)._coerce_to_smt_sort(other)
  File ".../crosshair/libimpl/builtinslib.py", line 357, in _coerce_to_smt_sort
    return cls._smt_promote_literal(input_value)
  File ".../crosshair/libimpl/builtinslib.py", line 1298, in _smt_promote_literal
    return z3.RealVal(literal)
  File ".../z3/z3.py", line 3262, in RealVal
    return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
  File ".../z3/z3core.py", line 2361, in Z3_mk_numeral
    _elems.Check(a0)
  File ".../z3/z3core.py", line 1554, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'parser error'

[Zac-HD]

New tests from https://github.com/HypothesisWorks/hypothesis/pull/4081 are also failing with this error, so it's probably my next wishlist item (behind the sets failure/s) 🙂

[pschanely]

Thanks for this! The prioritization guidance is super helpful too. Fixed in 0.0.67!

[Zac-HD]

I can confirm the fix works, and I love the way the diff of xfailed tests keeps shrinking 🤩

We're actually running low on important semantic issues, so I'd probably turn next to performance issues - there are some very slow tests that I've just skipped because they take several minutes, or hours, or don't finish at all within the 6h Actions time limit. Current commit with those is https://github.com/HypothesisWorks/hypothesis/pull/4034/commits/bb432101541c618762b1024b10e277658105baf8