SMTChecker: Support block.slotnum

[rodiazet]

Description

This PR introduce support for block.slotnum in the SMT solver. It’s moved to a separated PR as there is unresolved resource issue.

• Extend tx type constraints with block.slotnum.
• Increase Z3 resource limit.

Depends on #16881

AI Disclosure

• No AI tools were used

Claude Code, Anthropic's CLI for Claude (running on the Sonnet 5 model).

[rodiazet]

The problem was in the z3 library. It segfaults when built from sources. Detailed report below:

z3 4.13.3 macOS CI Segfault — Investigation Report

Symptom

CircleCI macOS jobs (smtCheckerTests) intermittently failed with
Error during interaction with the solver. The failure recurred across
several pipeline runs, always in tests going through the CHC/Spacer engine
(e.g. external_hash_known_code_state_unsafe_trusted,
aon_blog_post, abi_encode_with_selector_vs_sig).

Root cause

The z3 CLI subprocess invoked by SMTSolverCommand was crashing with
SIGSEGV (exit code 139), not returning any output, which
CHCSmtLib2Interface/Z3CHCSmtLib2Interface correctly reported as a solver
interaction error.

Confirmed via lldb, the crash is a null-pointer dereference inside z3 itself:

ast_manager::are_equal(a, b=0x0) at ast.cpp:1607
  <- model_evaluator::are_equal at model_evaluator.cpp:845
  <- mbp::mbp_array_tg::impl::elimwreq at src/qe/mbp/mbp_arrays_tg.cpp:199
  <- ... spacer::context::solve_core ... (CHC/Spacer array MBP path)

At mbp_arrays_tg.cpp:199, elimwreq() calls m_mdl.are_equal(j, i) where
i is drawn from p.get_diff_indices(indices). j cannot be null (guarded
by VERIFY(is_arr_write(...)) just above), so i is the null value — i.e.
get_diff_indices can populate the vector with a null expr* under some
circumstances. This is a bug in z3's own Spacer array
model-based-projection (MBP) code, deterministically reproducible with our
CI's exact CHC query and solver flags, and unrelated to Solidity's build
config.

Reproduced deterministically (5/5) with our project's exact CMake-based
from-source build (universal x86_64;arm64, Z3_BUILD_LIBZ3_SHARED=false).
Never reproduced (0/5) with the official prebuilt
z3-4.13.3-arm64-osx-13.7 release binary on the same query/flags.

Hypotheses ruled out

Each of the following was tested by rebuilding z3 from source with the
change applied, then running the crash query 5x for determinism:

Hypothesis	Test	Result
Optimization level (-O2/default RelWithDebInfo vs -O3/Release)	Explicit -DCMAKE_BUILD_TYPE=Release	Still crashes 5/5
Universal (fat) binary vs single-arch	arm64-only build	Still crashes 5/5
CMake build system vs official build tooling	Built via scripts/mk_unix_dist.py --arch=arm64 (the actual script the official Azure Pipelines release job runs — legacy mk_make.py/make, -O3 -DNDEBUG, single-arch, static lib)	Still crashes 5/5

The official release is built on Azure DevOps (scripts/release.yml,
MacBuildArm64 job, vmImage: macOS-13, released 2024-10-10), using an
Xcode/clang toolchain roughly 2-3 major versions older than what's
available locally (Apple clang 17 / macOS SDK 26.1 here). Since the
build system, flags, and architecture are now all ruled out as the
differentiator, the most likely remaining explanation is that this
z3-internal bug is sensitive to codegen/memory-layout differences between
compiler versions (e.g. pointer-hash-driven iteration order in z3's AST
hash tables), and just happens not to trigger with whatever code the
older official-build toolchain emitted. Reproducing that exact toolchain
was judged impractical (unsupported old Xcode on current macOS) and, per
discussion with the user, this line of investigation was stopped once the
build-system hypothesis was also ruled out — the bug is upstream in z3,
not in this project's configuration.

Fix applied

.circleci/osx_install_dependencies.sh: replaced the from-source z3 build
with a download of the official prebuilt z3-4.13.3-arm64-osx-13.7
release binary (checksum-validated), mirroring the existing cvc5
install pattern already in the same script. Safe because z3 is only ever
invoked as an external CLI subprocess (boost::process in
SMTSolverCommand.cpp) on macOS jobs — it is never linked into
solc/soltest (linking only happens if(EMSCRIPTEN)).

Committed on slotnum-formal as its own commit ("CI: Use official
prebuilt z3 binary on macOS instead of building from source"), isolated
from the other SMT changes on the branch.

Other changes kept on slotnum-formal

• Bumped z3 rlimit from 2,000,000 to 4,000,000 in
  SMTSolverCommand.cpp / Z3CHCSmtLib2Interface.cpp / Z3SMTLib2Interface.cpp
  to fix a separate, legitimate resource-limit flake unrelated to the crash.
• SMTEncoder/SymbolicState now properly encode block.slotnum in the
  transaction tuple, so it's a known member rather than an unsupported one.

Defensive block/tx member handling — parent branch only

SMTEncoder.cpp / SymbolicState.h (hasTxMember/hasMember) originally
made an unsupported block/tx member (like slotnum, before its tuple
encoding existed) produce an "unsupported expression" warning (error 2350)
instead of crashing. This was added on slotnum-formal, then reverted
there once proper encoding for block.slotnum was added, making the
fallback unnecessary — so it is not present in the current
slotnum-formal tree. It does still exist, un-reverted, at the tip of the
parent slotnum branch, which doesn't carry the tx-tuple encoding.

[cameel]

Why is this change dumped into an unrelated feature PR? Even if it was discovered during its implementation, it sounds like a the crash is not even triggered by slotnum (clanker's comment mentions external_hash_known_code_state_unsafe_trusted, aon_blog_post, abi_encode_with_selector_vs_sig). This should be a separate PR.

[rodiazet]

This is strictly related to the slotnum change. After increasing the resource limit (required after adding block.slotnum to libsolidity/formal) for the solver this library started crashing because it’s build locally in different environment then local I used for tests. There is a bug in the implementation described here. Better solution is to update the z3 version but not sure we wanna do it. It will probably introduce more updates in test results.

[blishko]

I agree with @cameel, it seems to me this PR is doing three (somewhat) unrelated things:

1. Changing the Z3 binary we use for OSX on CircleCI
2. Bumping resource limit for Z3
3. Actually adding support for slotnum

I did not quite get why we need to do the first two points (though at least the first one seems reasonable).
If the first two points are necessary, I also think they should be done in a separate PRs.

[cameel]

This is strictly related to the slotnum change.

It still does not sounds to me like it is. Z3 has a bug regardless of whether we trigger it or not. slotnum is not the only possible way to trigger it, is it? Those test names I cited seem to indicate otherwise.

In any case, switching to pre-built Z3 is more like CI configuration change. It's good that you put it in a separate commit at least, but I'd go further and in general avoid quietly bundling such changes into feature PRs. It's hard to keep up with what's happening in the codebase if one can't have a good guess at what a PR does from the title.

Better solution is to update the z3 version but not sure we wanna do it.

We do. We even discussed that on the call last week. @blishko wanted to do it pretty soon. But if switching to pre-built Z3 also fixes the bug, I think it's fine to do it regardless. The update sounded like it will be complicated.

[rodiazet]

Yes slotnum was a way to trigger it, of course not the only one probably.
Switching to prebuild is already merged with the explanation how it crashes and the repro described in the PR. I separated the Z3 query from our tests to trigger this bug without using solidity testing framework.

I would not separate the resource limit increasing change to its own PR because it’s strictly related to the change. It does not happen without block.slotnum addition to the tx type constraints.

[rodiazet]

This is the error when run without resource increasing.
https://app.circleci.com/pipelines/github/argotorg/solidity/43635/workflows/fd8d19c3-830f-4c40-bca6-585fc731f4c8/jobs/2092528

[cameel]

Why does the changelog only mention this configuration tweak and not the point of the PR, which is the fact that it adds slotnum support to SMTChecker?

[rodiazet]

Right. This should be added too.

[blishko]

Suggested change

	* SMTChecker: Support `block.slotnum` in BMC and CHC engines.
	* SMTChecker: Support `block.slotnum`.

No need to mention the engines.

[blishko]

Please revert the increase of Z3 limit and replace Z3 with Eldarica if some tests start to fail.