Unexpected checking results for functions with/without type annotations #234
Description
Expected vs actual behavior
We found some unexpected outputs when we add/remove/modify the type annotations of functions, which might be confusing. Here are some minimalized examples and their behaviors.
def arithmetic_op(a, b):
"""
post: True
"""
result = a + b
return result
# actual: /tmp/main.py:5: error: TypeError: when calling arithmetic_op('', '')
# expect: counterexamples like arithmetic_op('', 0)
def arithmetic_op(a: list, b: str):
"""
post: True
"""
result = a + b
return result
# actual: No counterexamples found.
# expect: counterexamples like arithmetic_op([], 0)
from typing import Optional
def arithmetic_op(a: 'int', b: 'Optional[complex]'):
"""
post: True
"""
result = a + b
return result
# actual: No counterexamples found.
# expect: counterexamples like arithmetic_op(0, None)
def func(a: 'str'):
"""
post: True
"""
return a(1)
# actual: No counterexamples found.
# expect: counterexamples like func('')
def func2(a: 'int'):
"""
post: True
"""
return a(1)
# actual: exception raised, Numeric operation on symbolic while not tracing
# expect: counterexamples like func2(1)