search

ethereum / solidity

Solidity, the Smart Contract Programming Language
https://soliditylang.org
GNU General Public License v3.0
23.23k stars 5.76k forks source link

Run SMT (or all) tests in absence of solvers to check the smtlib interface. #10519

Closed ekpyron closed 1 year ago

ekpyron commented 3 years ago

Doing so would have caught https://github.com/ethereum/solidity/issues/10436, resp. https://github.com/ethereum/solidity/pull/10494

We can either add some special run for this or we can just not skip the tests entirely if there is no solver, but just ignore the expectations.

(ping @leonardoalt for additional comments, if any)

ekpyron commented 3 years ago

We could actually run all our test files in general with the smtlib engine - it should be fast enough and would catch ICEs in the encoding part at least.

cameel commented 3 years ago

Running it on all tests will also be much easier when we replace the pragma with a command-line flag.

github-actions[bot] commented 1 year ago

This issue has been marked as stale due to inactivity for the last 90 days. It will be automatically closed in 7 days.

github-actions[bot] commented 1 year ago

Hi everyone! This issue has been automatically closed due to inactivity. If you think this issue is still relevant in the latest Solidity version and you have something to contribute, feel free to reopen. However, unless the issue is a concrete proposal that can be implemented, we recommend starting a language discussion on the forum instead.

cameel commented 1 year ago

Should we reopen this? Seems simple enough, we already have the CLI flag and also it's an SMT issue (and we wanted to exclude these, though most of them are not labeled).

ekpyron commented 1 year ago

Stop trying to rescue issues :-).