From d2924d83a2768ef749904d1d05a3b972b4c60436 Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Tue, 2 Jun 2020 15:37:45 +0200 Subject: [PATCH] Adding fixes for signedness warnings in smtutil --- libsmtutil/CVC4Interface.cpp | 2 +- libsmtutil/SMTLib2Interface.cpp | 2 +- libsmtutil/Z3Interface.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 4c1ef378a..2af305e0e 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -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]); } diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index 4e81444fe..94da07aec 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -151,7 +151,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 b42bc4765..fed82cc8b 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -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")