Repository navigation
Conversation
SMTLib2Context::toSExpr printed every expression without arguments as its name. An empty tuple is a zero-argument `tuple_constructor`, which is never declared, so the solver rejected the whole query and every target of the contract was reported unproved. The zero-argument branch added in argotorg#15025 only existed in Z3Interface, which was removed in 0.8.29. Fixes argotorg#17192.
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
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.
Description
Fixes #17192.
SMTLib2Context::toSExprprinted a zero-argumenttuple_constructor(empty tuple) as the bare, undeclaredtuple_constructor, so the solver rejected the query and all CHC targets of the contract (and BMC targets after the construct) ended up unproved. This ports to the SMT-LIB printer the zero-argument branch that #15025 added toZ3Interface::toZ3Expr: the empty tuple is now printed as the constructor of its tuple sort (|tuple[]|).The existing tests
ternary_operator_with_tupleandternary_operator_with_functionshad no verification target, so no query reached the solver and they passed with or without the fix. They now contain an assertion and run with CHC only. A new test coversabi.encodeCall(f, ()). Without the fix, the three tests reportCHC: Error during interaction with the solverand their targets as unproved; with the fix, both targets of each test are proved safe (z3 4.13.3).isoltest -t "smtCheckerTests/*": 1432/1438 passed, 6 skipped, 0 failures (CI imagesolidity-buildpack-deps:ubuntu2404-8, z3 4.13.3)scripts/check_style.sh: cleanChecklist
AI Disclosure
Claude (Anthropic) was used to check the tests and draft this description. I reviewed, built and tested every change.