5 files changed, 58 insertions, 24 deletions

diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index 84d36de0..6cb91483 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -52,18 +52,23 @@ void CVC4Interface::pop()
 
 void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
-	CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
-	m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
+	if (!m_functions.count(_name))
+	{
+		CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
+		m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
+	}
 }
 
 void CVC4Interface::declareInteger(string _name)
 {
-	m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
 }
 
 void CVC4Interface::declareBool(string _name)
 {
-	m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
 }
 
 void CVC4Interface::addAssertion(Expression const& _expr)
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 109c8dbe..17b50a38 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",
+		"<result>",
 		&_value
 	);
 	checkCondition(
 		_value > SymbolicIntVariable::maxValue(_type),
 		_location,
 		"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
-		"value",
+		"<result>",
 		&_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", "<result>", &right);
 			m_interface->addAssertion(right != 0);
 		}
 
@@ -601,15 +601,23 @@ void SMTChecker::checkCondition(
 		message << _description << " happens here";
 		if (m_currentFunction)
 		{
-			message << " for:\n";
+			std::ostringstream modelMessage;
+			modelMessage << "  for:\n";
 			solAssert(values.size() == expressionNames.size(), "");
+			map<string, string> sortedModel;
 			for (size_t i = 0; i < values.size(); ++i)
 				if (expressionsToEvaluate.at(i).name != values.at(i))
-					message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
+					sortedModel[expressionNames.at(i)] = values.at(i);
+
+			for (auto const& eval: sortedModel)
+				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
+			m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation()));
 		}
 		else
+		{
 			message << ".";
-		m_errorReporter.warning(_location, message.str() + loopComment);
+			m_errorReporter.warning(_location, message.str() + loopComment);
+		}
 		break;
 	}
 	case smt::CheckResult::UNSATISFIABLE:
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 8cac3cc6..a6c1f87c 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -47,6 +47,8 @@ void SMTLib2Interface::reset()
 {
 	m_accumulatedOutput.clear();
 	m_accumulatedOutput.emplace_back();
+	m_constants.clear();
+	m_functions.clear();
 	write("(set-option :produce-models true)");
 	write("(set-logic QF_UFLIA)");
 }
@@ -64,25 +66,38 @@ void SMTLib2Interface::pop()
 
 void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
-	write(
-		"(declare-fun |" +
-		_name +
-		"| (" +
-		(_domain == Sort::Int ? "Int" : "Bool") +
-		") " +
-		(_codomain == Sort::Int ? "Int" : "Bool") +
-		")"
-	);
+	// TODO Use domain and codomain as key as well
+	if (!m_functions.count(_name))
+	{
+		m_functions.insert(_name);
+		write(
+			"(declare-fun |" +
+			_name +
+			"| (" +
+			(_domain == Sort::Int ? "Int" : "Bool") +
+			") " +
+			(_codomain == Sort::Int ? "Int" : "Bool") +
+			")"
+		);
+	}
 }
 
 void SMTLib2Interface::declareInteger(string _name)
 {
-	write("(declare-const |" + _name + "| Int)");
+	if (!m_constants.count(_name))
+	{
+		m_constants.insert(_name);
+		write("(declare-const |" + _name + "| Int)");
+	}
 }
 
 void SMTLib2Interface::declareBool(string _name)
 {
-	write("(declare-const |" + _name + "| Bool)");
+	if (!m_constants.count(_name))
+	{
+		m_constants.insert(_name);
+		write("(declare-const |" + _name + "| Bool)");
+	}
 }
 
 void SMTLib2Interface::addAssertion(Expression const& _expr)
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 61071fe5..eb876a7f 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -30,6 +30,7 @@
 #include <string>
 #include <vector>
 #include <cstdio>
+#include <set>
 
 namespace dev
 {
@@ -68,6 +69,8 @@ private:
 
 	ReadCallback::Callback m_queryCallback;
 	std::vector<std::string> m_accumulatedOutput;
+	std::set<std::string> m_constants;
+	std::set<std::string> m_functions;
 };
 
 }
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 784fbd28..747c9172 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -53,17 +53,20 @@ void Z3Interface::pop()
 
 void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
-	m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
+	if (!m_functions.count(_name))
+		m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
 }
 
 void Z3Interface::declareInteger(string _name)
 {
-	m_constants.insert({_name, m_context.int_const(_name.c_str())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.int_const(_name.c_str())});
 }
 
 void Z3Interface::declareBool(string _name)
 {
-	m_constants.insert({_name, m_context.bool_const(_name.c_str())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.bool_const(_name.c_str())});
 }
 
 void Z3Interface::addAssertion(Expression const& _expr)