From e21eab96f385a77ef04bce8cc1055fabad0aa9b3 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Thu, 30 Nov 2023 17:02:42 +0100 Subject: [PATCH] apply CR comments --- libsolidity/formal/PredicateInstance.cpp | 2 +- libsolidity/formal/SMTEncoder.cpp | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 72351ae3b312..a3be210fbfdb 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -51,7 +51,7 @@ smtutil::Expression nondetInterface( { auto const& state = _context.state(); std::vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(), - state.abi(), state.bytesConcat(0), state.crypto()}; + state.abi(), state.bytesConcat(), state.crypto()}; return _pred( stateExprs + std::vector{_context.state().state(_preIdx)} + diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index a67918d23f77..45c456185d4a 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -810,7 +810,7 @@ void SMTEncoder::visitBytesConcat(FunctionCall const& _funCall) if (args.at(i)) symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i))); - std::optional arg; + smtutil::Expression arg; if (inTypes.size() == 1) arg = expr(*args.at(0), inTypes.at(0)); else @@ -824,8 +824,6 @@ void SMTEncoder::visitBytesConcat(FunctionCall const& _funCall) auto out = smtutil::Expression::select(symbFunction, *arg); defineExpr(_funCall, out); - - return; } void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)