Fixing additional signedness errors after adding -Wsign-conversion flag

Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
This commit is contained in:
Djordje Mijovic
2020-07-09 17:22:45 +02:00
co-authored by Kamil Śliwak
parent 3c57e04751
commit 547590b972
12 changed files with 20 additions and 20 deletions
+1 -1
View File
@@ -191,7 +191,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]);
else if (n == "int2bv")
{
size_t size = std::stoi(_expr.arguments[1].name);
size_t size = std::stoul(_expr.arguments[1].name);
auto i2bvOp = m_context.mkConst(CVC4::IntToBitVector(size));
// CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
return m_context.mkExpr(
+1 -1
View File
@@ -139,7 +139,7 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
std::string sexpr = "(";
if (_expr.name == "int2bv")
{
size_t size = std::stoi(_expr.arguments[1].name);
size_t size = std::stoul(_expr.arguments[1].name);
auto arg = toSExpr(_expr.arguments.front());
auto int2bv = "(_ int2bv " + to_string(size) + ")";
// Some solvers treat all BVs as unsigned, so we need to manually apply 2's complement if needed.
+1 -1
View File
@@ -184,7 +184,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] & arguments[1];
else if (n == "int2bv")
{
size_t size = std::stoi(_expr.arguments[1].name);
size_t size = std::stoul(_expr.arguments[1].name);
return z3::int2bv(size, arguments[0]);
}
else if (n == "bv2int")