From 2fe143f7d0d0480bc39259adaf4248a6ca1e57ff Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 11 May 2022 17:16:10 +0200 Subject: [PATCH] add changelog entry and docs note --- Changelog.md | 1 + docs/smtchecker.rst | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/Changelog.md b/Changelog.md index 2e4bbccc4..dcb364610 100644 --- a/Changelog.md +++ b/Changelog.md @@ -15,6 +15,7 @@ Bugfixes: * Type Checker: Properly check restrictions of ``using ... global`` in conjunction with libraries. * Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`. * SMTChecker: Fix bug when z3 is selected but not available at runtime. + * SMTChecker: Fix ABI compatibility with z3 >=4.8.16. * TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``. * View Pure Checker: Mark ``returndatasize`` and ``returndatacopy`` as view to disallow them in inline assembly blocks in pure functions. diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 5093408a7..caa901713 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -629,6 +629,11 @@ option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option - if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6); - statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler. +.. note:: + z3 version 4.8.16 broke ABI compatibility with previous versions and cannot + be used with solc <=0.8.13. If you are using z3 >=4.8.16 please use solc + >=0.8.14. + Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety of environments, including in the browser, most users will almost never need to be concerned about this option. More advanced users might apply this option to try