aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp12
-rw-r--r--libsolidity/formal/SMTChecker.h4
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);