From b588134840bf604ed4fa6031fb06a89cbbd13bcd Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leonardoaltt@gmail.com>
Date: Mon, 18 Dec 2017 17:31:27 +0100
Subject: [SMTChecker] Fix typo in the code (satisifable->satisfiable)

---
 libsolidity/formal/SMTChecker.cpp | 12 ++++++------
 libsolidity/formal/SMTChecker.h   |  4 ++--
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index d4887a3d..a8529795 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -560,7 +560,7 @@ void SMTChecker::checkCondition(
 	}
 	smt::CheckResult result;
 	vector<string> values;
-	tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate);
+	tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
 
 	string conditionalComment;
 	if (m_conditionalExecutionHappened)
@@ -607,12 +607,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 
 	m_interface->push();
 	addPathConjoinedExpression(expr(_condition));
-	auto positiveResult = checkSatisifable();
+	auto positiveResult = checkSatisfiable();
 	m_interface->pop();
 
 	m_interface->push();
 	addPathConjoinedExpression(!expr(_condition));
-	auto negatedResult = checkSatisifable();
+	auto negatedResult = checkSatisfiable();
 	m_interface->pop();
 
 	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
@@ -642,7 +642,7 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 }
 
 pair<smt::CheckResult, vector<string>>
-SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
+SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
 {
 	smt::CheckResult result;
 	vector<string> values;
@@ -672,9 +672,9 @@ SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _exp
 	return make_pair(result, values);
 }
 
-smt::CheckResult SMTChecker::checkSatisifable()
+smt::CheckResult SMTChecker::checkSatisfiable()
 {
-	return checkSatisifableAndGenerateModel({}).first;
+	return checkSatisfiableAndGenerateModel({}).first;
 }
 
 void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 539221cc..d4c2cf6f 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -100,9 +100,9 @@ private:
 
 
 	std::pair<smt::CheckResult, std::vector<std::string>>
-	checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
+	checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
 
-	smt::CheckResult checkSatisifable();
+	smt::CheckResult checkSatisfiable();
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void resetVariables(std::vector<Declaration const*> _variables);
-- 
cgit