cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Adding fixes for signedness warnings in smtutil

Browse Source
This commit is contained in:
Djordje Mijovic 2020-06-02 15:37:45 +02:00
parent e7f97cf3ac
commit d2924d83a2
3 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CVC4Interface.cpp
View File

@ -201,7 +201,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
size_t index = std::stoi(_expr.arguments[1].name);
size_t index = std::stoul(_expr.arguments[1].name);
CVC4::Expr s = dt[0][index].getSelector();
return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]);
}

2
libsmtutil/SMTLib2Interface.cpp
View File

@ -151,7 +151,7 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
{
smtAssert(_expr.arguments.size() == 2, "");
auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.arguments.at(0).sort);
unsigned index = std::stoi(_expr.arguments.at(1).name);
size_t index = std::stoul(_expr.arguments.at(1).name);
smtAssert(index < tupleSort->members.size(), "");
sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0));
}

2
libsmtutil/Z3Interface.cpp
View File

@ -194,7 +194,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
}
else if (n == "tuple_get")
{
size_t index = std::stoi(_expr.arguments[1].name);
size_t index = stoul(_expr.arguments[1].name);
return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]);
}
else if (n == "tuple_constructor")