Skip to content

Commit

Permalink
apply CR comments
Browse files Browse the repository at this point in the history
  • Loading branch information
pgebal committed Dec 4, 2023
1 parent 8aad1b4 commit e21eab9
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 4 deletions.
2 changes: 1 addition & 1 deletion libsolidity/formal/PredicateInstance.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ smtutil::Expression nondetInterface(
{
auto const& state = _context.state();
std::vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(),
state.abi(), state.bytesConcat(0), state.crypto()};
state.abi(), state.bytesConcat(), state.crypto()};
return _pred(
stateExprs +
std::vector<smtutil::Expression>{_context.state().state(_preIdx)} +
Expand Down
4 changes: 1 addition & 3 deletions libsolidity/formal/SMTEncoder.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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<smtutil::Expression> arg;
smtutil::Expression arg;
if (inTypes.size() == 1)
arg = expr(*args.at(0), inTypes.at(0));
else
Expand All @@ -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)
Expand Down

0 comments on commit e21eab9

Please sign in to comment.