prosyslab-classroom / cs424-program-reasoning

45 stars 20 forks source link

[Question][Hw3] Uninterpreted error #168

Closed githubqookie closed 4 months ago

githubqookie commented 11 months ago

Name:김승기

Since I'm having an uninterpreted error of variable add, I checked the debug.smt2 . But I can't find any rule such that add is not in the range of quantifier. Can I get some help? [code]

image

[ll code]

image

[debug.smt2]

image image

[error message]

image
githubqookie commented 11 months ago

Solved, It was about the string error "%add" vs "add"