swtv-kaist / cs458-fall22

1 stars 0 forks source link

[HW7] 1.5: Input values are limited to int => BV and LIA should conclude into same result #23

Closed retroinspect closed 1 year ago

retroinspect commented 1 year ago

From the provided C code, input value a, b is limited to integer domain. Therefore I expect BV and LIA should conclude into same result. Does the question mean to expand the input domain?

moonzoo commented 1 year ago

Hint. Do you really think that "integer domain" in BV and LIA are the same?