From 19e067465a058ca9f40238cb3a928a1113531c9d Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 5 Oct 2017 15:23:25 +0200 Subject: Unary operators and division. --- libsolidity/formal/Z3Interface.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'libsolidity/formal/Z3Interface.cpp') diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index e5c1aef4..769e6edb 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -127,7 +127,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) {">=", 2}, {"+", 2}, {"-", 2}, - {"*", 2} + {"*", 2}, + {"/", 2} }; string const& n = _expr.name; if (m_functions.count(n)) @@ -173,6 +174,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return arguments[0] - arguments[1]; else if (n == "*") return arguments[0] * arguments[1]; + else if (n == "/") + return arguments[0] / arguments[1]; // Cannot reach here. solAssert(false, ""); return arguments[0]; -- cgit v1.2.3