SMT checker: Fix pop() assertion to match push/pop frame stack#16661
Closed
cuiweixie wants to merge 1 commit intoargotorg:developfrom
Closed
SMT checker: Fix pop() assertion to match push/pop frame stack#16661cuiweixie wants to merge 1 commit intoargotorg:developfrom
cuiweixie wants to merge 1 commit intoargotorg:developfrom
Conversation
push() bookmarks the active command deque size in m_frameLimits; pop() must restore trailing commands relative to that limit. Checking m_commands.empty() could fail right after opening a stack frame during which nothing was asserted yet—the deque can legitimately remain empty across push/pop boundaries. Replace the guard with a non-empty m_frameLimits check instead so stray pop calls are still diagnosed without blocking valid checker sessions.
Collaborator
|
Closing the PR because it ignores the mandatory disclosures we put into place recently. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
SMTLib2Commands::pop()usedsmtAssert(!m_commands.empty())before reading the bookmarked deque size offm_frameLimits. That does not mirror whatpush()guarantees:push()always pushes the current deque size ontom_frameLimits, but the deque may legitimately remain empty across a bracket if no commands were flushed while the inner frame stayed open.Fix
Replace the precondition with
smtAssert(!m_frameLimits.empty()), which validates push/pop bookkeeping and still catches unbalanced pops when the stack is drained.References
Touches
libsmtutil/SMTLib2Interface.cpponly.