diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 87184714f..7735d5a16 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -246,7 +246,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]); } diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index bc37ffb6c..ce1efb5f6 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -184,7 +184,7 @@ string SMTLib2Interface::toSExpr(Expression const& _expr) { smtAssert(_expr.arguments.size() == 2, ""); auto tupleSort = dynamic_pointer_cast(_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)); } diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 1337b7b20..a71d008ab 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -207,7 +207,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")