[SMTChecker] Helper functions to add an expression to the solver conjoined with or implied by the current path conditions

2 files changed, 19 insertions, 5 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 61cb110e..d4887a3d 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -345,14 +345,14 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		solAssert(args.size() == 1, "");
 		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
 		checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
-		m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0])));
+		addPathImpliedExpression(expr(*args[0]));
 	}
 	else if (funType.kind() == FunctionType::Kind::Require)
 	{
 		solAssert(args.size() == 1, "");
 		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
 		checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
-		m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0])));
+		addPathImpliedExpression(expr(*args[0]));
 	}
 }
 
@@ -534,7 +534,7 @@ void SMTChecker::checkCondition(
 )
 {
 	m_interface->push();
-	m_interface->addAssertion(currentPathConditions() && _condition);
+	addPathConjoinedExpression(_condition);
 
 	vector<smt::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
@@ -606,12 +606,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 		return;
 
 	m_interface->push();
-	m_interface->addAssertion(currentPathConditions() && expr(_condition));
+	addPathConjoinedExpression(expr(_condition));
 	auto positiveResult = checkSatisifable();
 	m_interface->pop();
 
 	m_interface->push();
-	m_interface->addAssertion(currentPathConditions() && !expr(_condition));
+	addPathConjoinedExpression(!expr(_condition));
 	auto negatedResult = checkSatisifable();
 	m_interface->pop();
 
@@ -847,3 +847,13 @@ smt::Expression SMTChecker::currentPathConditions()
 		return smt::Expression(true);
 	return m_pathConditions.back();
 }
+
+void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
+{
+	m_interface->addAssertion(currentPathConditions() && _e);
+}
+
+void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
+{
+	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 7f990b97..539221cc 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -152,6 +152,10 @@ private:
 	void popPathCondition();
 	/// Returns the conjunction of all path conditions or True if empty
 	smt::Expression currentPathConditions();
+	/// Conjoin the current path conditions with the given parameter and add to the solver
+	void addPathConjoinedExpression(smt::Expression const& _e);
+	/// Add to the solver: the given expression implied by the current path conditions
+	void addPathImpliedExpression(smt::Expression const& _e);
 
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;