From b0acb5761c25cc7ff610db8eb3f513af5f2c24ac Mon Sep 17 00:00:00 2001 From: Asuka Date: Thu, 18 Jun 2026 10:17:42 +0800 Subject: [PATCH] fix(smtchecker): stop ICE on TRON crypto builtins The 6 TRON crypto/zk builtins were routed into visitCryptoFunction, which solAssert(false)s on them, crashing the model checker. Let them fall to the default unsupported-call warning like the other TRON builtins. --- libsolidity/formal/SMTEncoder.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b5ad4b3b50b2..1c0808cc017b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -670,12 +670,6 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: - case FunctionType::Kind::ValidateMultiSign: - case FunctionType::Kind::BatchValidateSign: - case FunctionType::Kind::VerifyBurnProof: - case FunctionType::Kind::VerifyTransferProof: - case FunctionType::Kind::VerifyMintProof: - case FunctionType::Kind::PedersenHash: case FunctionType::Kind::SHA256: case FunctionType::Kind::RIPEMD160: visitCryptoFunction(_funCall); @@ -731,6 +725,12 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareDelegateCall: default: + // The TRON-specific builtins (freeze/unfreeze, vote, the various V2 calls, + // validatemultisign/batchvalidatesign, the zk-proof verifiers, pedersenhash, ...) + // are not modeled here: we only emit the warning below. Their state side effects + // are not havoc'd in this branch; soundness for state mutation across unmodeled + // calls is instead handled by the engine-level reset logic (CHC::unknownFunctionCall + // / makeOutsideFunctionCall and BMC's resetStateVariables paths). m_unsupportedErrors.warning( 4588_error, _funCall.location(),