Open
Description
Expected vs actual behavior
We'd expect a counterexample in this case, but not the one we get:
example:
from typing import Sequence
def try_index(dd: Sequence[int], idx=0) -> None:
"""
post: True
"""
return dd[idx]
actual output:
/tmp/main.py:6: error: TypeError: indices must be integers or slices, not <class 'crosshair.libimpl.builtinslib.SymbolicObject'> when calling try_index((), idx = '')
It's ok for crosshair to try various types for the idx
param (it has a default but can legitimately be any type), but we expect the counterexample to be some sort of regular Python type, not a CrossHair internal type.
To Reproduce
https://crosshair-web.org/?crosshair=0.1&python=3.8&flags=verbose&gist=015bea7c81fa2ebaf9bb7d01ccb655d5
Metadata
Metadata
Assignees
Labels
No labels