Fix signed division.

2 files changed, 20 insertions, 2 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 9e2cf908..c20c63c6 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -401,13 +401,14 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 	{
 		solAssert(_op.annotation().commonType, "");
 		solAssert(_op.annotation().commonType->category() == Type::Category::Integer, "");
+		auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
 		smt::Expression left(expr(_op.leftExpression()));
 		smt::Expression right(expr(_op.rightExpression()));
 		Token::Value op = _op.getOperator();
 		smt::Expression value(
 			op == Token::Add ? left + right :
 			op == Token::Sub ? left - right :
-			op == Token::Div ? left / right :
+			op == Token::Div ? division(left, right, intType) :
 			/*op == Token::Mul*/ left * right
 		);
 
@@ -417,7 +418,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 			m_interface->addAssertion(right != 0);
 		}
 
-		checkUnderOverflow(value, dynamic_cast<IntegerType const&>(*_op.annotation().commonType), _op.location());
+		checkUnderOverflow(value, intType, _op.location());
 
 		defineExpr(_op, value);
 		break;
@@ -475,6 +476,19 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 					);
 }
 
+smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type)
+{
+	// Signed division in SMTLIB2 rounds differently for negative division.
+	if (_type.isSigned())
+		return (smt::Expression::ite(
+			_left >= 0,
+			smt::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
+			smt::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
+		));
+	else
+		return _left / _right;
+}
+
 void SMTChecker::assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location)
 {
 	assignment(_variable, expr(_value), _location);
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index cc3aca81..e7481cca 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -67,6 +67,10 @@ private:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	/// Division expression in the given type. Requires special treatment because
+	/// of rounding for signed division.
+	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
+
 	void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location);
 	void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);