From 18ae0c3d784cb587d50bdfc1f33e200fd97f2676 Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Wed, 4 Oct 2017 14:23:27 +0100
Subject: SMT enforce variable types

---
 libsolidity/formal/SMTLib2Interface.cpp | 9 ++++++++-
 libsolidity/formal/SMTLib2Interface.h   | 8 ++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index cbd766fb..c627057a 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -64,6 +64,8 @@ void SMTLib2Interface::pop()
 
 Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
 {
+	solAssert(!m_variables.count(_name), "");
+	m_variables[_name] = SMTVariableType::Function;
 	write(
 		"(declare-fun |" +
 		_name +
@@ -78,12 +80,16 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
 
 Expression SMTLib2Interface::newInteger(string _name)
 {
+	solAssert(!m_variables.count(_name), "");
+	m_variables[_name] = SMTVariableType::Integer;
 	write("(declare-const |" + _name + "| Int)");
 	return SolverInterface::newInteger(move(_name));
 }
 
 Expression SMTLib2Interface::newBool(string _name)
 {
+	solAssert(!m_variables.count(_name), "");
+	m_variables[_name] = SMTVariableType::Bool;
 	write("(declare-const |" + _name + "| Bool)");
 	return SolverInterface::newBool(std::move(_name));
 }
@@ -145,7 +151,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
 		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
 		{
 			auto const& e = _expressionsToEvaluate.at(i);
-			// TODO they don't have to be ints...
+			solAssert(m_variables.count(e.name), "");
+			solAssert(m_variables[e.name] == SMTVariableType::Integer, "");
 			command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
 			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 63188acd..e827449f 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -68,6 +68,14 @@ private:
 
 	ReadCallback::Callback m_queryCallback;
 	std::vector<std::string> m_accumulatedOutput;
+
+	enum class SMTVariableType {
+		Function,
+		Integer,
+		Bool
+	};
+
+	std::map<std::string,SMTVariableType> m_variables;
 };
 
 }
-- 
cgit