You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Both of these calls to yices should produce a counter example because we uninterpreted g in both. We know saw knows that g exists because saw would otherwise complain saying "Could not resolve name: g", but this does not happen. However, saw does not uninterpret g, nor does it unfold f when we try to print the term.
The text was updated successfully, but these errors were encountered:
I suspect that the naming environment is getting screwed up when we import an external saw-core file. I don't quite understand what's going on here yet, but something is definitely wrong under the surface. We should probably add some code (at least temporarily) to check and enforce the intended invariants on our naming environment.
I think #1257 is also related; in that thread I mentioned some design questions about how should we handle re-import of external saw-core files that contain defined constants.
This may be a bit related to #1044.
Basically,
saw
seems to know that symbol names exist in imported saw core files, but it doesn't act on them. For example:Both of these calls to yices should produce a counter example because we uninterpreted
g
in both. We knowsaw
knows thatg
exists becausesaw
would otherwise complain saying "Could not resolve name: g", but this does not happen. However,saw
does not uninterpretg
, nor does it unfoldf
when we try to print the term.The text was updated successfully, but these errors were encountered: