From b6a265551335edeff2f4e43f4a249fabba5381d7 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 1 Aug 2018 23:27:11 +0200 Subject: Replace "value" by "" in the SMT model --- libsolidity/formal/SMTChecker.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 109c8dbe..15300bc6 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -252,14 +252,14 @@ void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _ _value < SymbolicIntVariable::minValue(_type), _location, "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", - "value", + "", &_value ); checkCondition( _value > SymbolicIntVariable::maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", - "value", + "", &_value ); } @@ -437,7 +437,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) if (_op.getOperator() == Token::Div) { - checkCondition(right == 0, _op.location(), "Division by zero", "value", &right); + checkCondition(right == 0, _op.location(), "Division by zero", "", &right); m_interface->addAssertion(right != 0); } -- cgit