6 files changed, 37 insertions, 23 deletions
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index 7f214687..4e6bcbcb 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -25,13 +25,15 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
-SSAVariable::SSAVariable(Declaration const* _decl,
-	smt::SolverInterface& _interface)
+SSAVariable::SSAVariable(
+	Declaration const* _decl,
+	smt::SolverInterface& _interface
+)
 {
 	resetIndex();
 
 	if (dynamic_cast<IntegerType const*>(_decl->type().get()))
-		m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface);
+		m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
 	else
 	{
 		solAssert(false, "");
@@ -62,10 +64,10 @@ int SSAVariable::next() const
 
 void SSAVariable::setZeroValue()
 {
-	m_symbVar->setZeroValue(index());
+	m_symbolicVar->setZeroValue(index());
 }
 
 void SSAVariable::setUnknownValue()
 {
-	m_symbVar->setUnknownValue(index());
+	m_symbolicVar->setUnknownValue(index());
 }
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index b87693c2..4ec92aa1 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -36,8 +36,10 @@ class SSAVariable
 public:
 	/// @param _decl Used to determine the type and forwarded to the symbolic var.
 	/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
-	explicit SSAVariable(Declaration const* _decl,
-		smt::SolverInterface& _interface);
+	SSAVariable(
+		Declaration const* _decl,
+		smt::SolverInterface& _interface
+	);
 	SSAVariable(SSAVariable const&) = default;
 	SSAVariable(SSAVariable&&) = default;
 	SSAVariable& operator=(SSAVariable const&) = default;
@@ -45,7 +47,9 @@ public:
 
 	void resetIndex();
 
+	/// This function returns the current index of this SSA variable.
 	int index() const;
+	/// This function returns the next free index of this SSA variable.
 	int next() const;
 
 	int operator++()
@@ -74,10 +78,10 @@ public:
 private:
 	smt::Expression valueAtSequence(int _seq) const
 	{
-		return (*m_symbVar)(_seq);
+		return (*m_symbolicVar)(_seq);
 	}
 
-	std::shared_ptr<SymbolicVariable> m_symbVar = nullptr;
+	std::shared_ptr<SymbolicVariable> m_symbolicVar = nullptr;
 	int m_currentSequenceCounter;
 	/// The next free sequence counter is a shared pointer because we want
 	/// the copy and the copied to share it.
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index c206f1cd..d08dc155 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -23,9 +23,11 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
-SymbolicIntVariable::SymbolicIntVariable(Declaration const* _decl,
-	smt::SolverInterface&_interface)
-	: SymbolicVariable(_decl, _interface)
+SymbolicIntVariable::SymbolicIntVariable(
+	Declaration const* _decl,
+	smt::SolverInterface& _interface
+):
+	SymbolicVariable(_decl, _interface)
 {
 	solAssert(m_declaration->type()->category() == Type::Category::Integer, "");
 	m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int));
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index 0066bb75..8a9b5d5d 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -29,11 +29,13 @@ namespace solidity
 /**
  * Specialization of SymbolicVariable for Integers
  */
-class SymbolicIntVariable : public SymbolicVariable
+class SymbolicIntVariable: public SymbolicVariable
 {
 public:
-	explicit SymbolicIntVariable(Declaration const* _decl,
-		smt::SolverInterface& _interface);
+	SymbolicIntVariable(
+		Declaration const* _decl,
+		smt::SolverInterface& _interface
+	);
 	SymbolicIntVariable(SymbolicIntVariable const&) = default;
 	SymbolicIntVariable(SymbolicIntVariable&&) = default;
 	SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default;
@@ -41,7 +43,7 @@ public:
 
 	/// Sets the var to 0.
 	void setZeroValue(int _seq);
-	/// Sets the valid interval for the var.
+	/// Sets the variable to the full valid value range.
 	void setUnknownValue(int _seq);
 
 	static smt::Expression minValue(IntegerType const& _t);
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
index 13f5d9b6..629049ea 100644
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -23,9 +23,11 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
-SymbolicVariable::SymbolicVariable(Declaration const* _decl,
-	smt::SolverInterface& _interface)
-	: m_declaration(_decl),
+SymbolicVariable::SymbolicVariable(
+	Declaration const* _decl,
+	smt::SolverInterface& _interface
+):
+	m_declaration(_decl),
 	m_interface(_interface)
 {
 }
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 66633b73..2b59e57a 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -36,8 +36,10 @@ class Declaration;
 class SymbolicVariable
 {
 public:
-	explicit SymbolicVariable(Declaration const* _decl,
-		smt::SolverInterface& _interface);
+	SymbolicVariable(
+		Declaration const* _decl,
+		smt::SolverInterface& _interface
+	);
 	SymbolicVariable(SymbolicVariable const&) = default;
 	SymbolicVariable(SymbolicVariable&&) = default;
 	SymbolicVariable& operator=(SymbolicVariable const&) = default;
@@ -52,8 +54,8 @@ public:
 
 	/// Sets the var to the default value of its type.
 	virtual void setZeroValue(int _seq) = 0;
-	/// The unknown value depends on the type. For example, an interval is set for Integers.
-	/// This is decided by the subclasses.
+	/// The unknown value is the full range of valid values,
+	/// and that's sub-type dependent.
 	virtual void setUnknownValue(int _seq) = 0;
 
 protected: