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

Replace real division by integer division

Browse Source
This commit is contained in:
Leo Alt 2021-05-18 19:47:00 +02:00
parent fdf4c1ed9a
commit 3a0358bfb7
3 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CVC4Interface.cpp
View File

@ -188,7 +188,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]);
else if (n == "*")
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
else if (n == "/")
else if (n == "div")
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
else if (n == "mod")
return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);

4
libsmtutil/SolverInterface.h
View File

@ -95,7 +95,7 @@ public:
{"+", 2},
{"-", 2},
{"*", 2},
{"/", 2},
{"div", 2},
{"mod", 2},
{"bvnot", 1},
{"bvand", 2},
@ -300,7 +300,7 @@ public:
friend Expression operator/(Expression _a, Expression _b)
{
auto intSort = _a.sort;
return Expression("/", {std::move(_a), std::move(_b)}, intSort);
return Expression("div", {std::move(_a), std::move(_b)}, intSort);
}
friend Expression operator%(Expression _a, Expression _b)
{

2
libsmtutil/Z3Interface.cpp
View File

@ -207,7 +207,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] - arguments[1];
else if (n == "*")
return arguments[0] * arguments[1];
else if (n == "/")
else if (n == "div")
return arguments[0] / arguments[1];
else if (n == "mod")
return z3::mod(arguments[0], arguments[1]);