Skip to content

Unexpected counterexample when indexing a symbolic sequence by a object of unknown type #200

Open
@pschanely

Description

@pschanely

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

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions