Merge pull request #13009 from ethereum/smt_support_z3_16

Support new z3 AST node

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.
 

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

libsmtutil/Z3Interface.cpp

@@ -298,6 +298,7 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
 		arguments.push_back(fromZ3Expr(_expr.arg(i)));
 
 	auto kind = _expr.decl().decl_kind();
+
 	if (_expr.is_ite())
 		return Expression::ite(arguments[0], arguments[1], arguments[2]);
 	else if (_expr.is_not())
@@ -371,7 +372,10 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
 		return Expression("dt_accessor_" + _expr.decl().name().str(), arguments, sort);
 	else if (kind == Z3_OP_DT_IS)
 		return Expression("dt_is", {arguments.at(0)}, sort);
-	else if (kind == Z3_OP_UNINTERPRETED)
+	else if (
+		kind == Z3_OP_UNINTERPRETED ||
+		kind == Z3_OP_RECURSIVE
+	)
 		return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));
 
 	smtAssert(false, "");