1 files changed, 14 insertions, 9 deletions

diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index ae9f32e9..d7f86cbc 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -31,20 +31,25 @@
 #include <string>
 #include <vector>
 
+namespace langutil
+{
+class ErrorReporter;
+struct SourceLocation;
+}
+
 namespace dev
 {
 namespace solidity
 {
 
 class VariableUsage;
-class ErrorReporter;
 
 class SMTChecker: private ASTConstVisitor
 {
 public:
-	SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
+	SMTChecker(langutil::ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
 
-	void analyze(SourceUnit const& _sources, std::shared_ptr<Scanner> const& _scanner);
+	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
 
 private:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
@@ -89,8 +94,8 @@ private:
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
 
-	void assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location);
-	void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
+	void assignment(VariableDeclaration const& _variable, Expression const& _value, langutil::SourceLocation const& _location);
+	void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, langutil::SourceLocation const& _location);
 
 	/// Maps a variable to an SSA index.
 	using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
@@ -104,7 +109,7 @@ private:
 	/// Check that a condition can be satisfied.
 	void checkCondition(
 		smt::Expression _condition,
-		SourceLocation const& _location,
+		langutil::SourceLocation const& _location,
 		std::string const& _description,
 		std::string const& _additionalValueName = "",
 		smt::Expression* _additionalValue = nullptr
@@ -117,7 +122,7 @@ private:
 		std::string const& _description
 	);
 	/// Checks that the value is in the range given by the type.
-	void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, SourceLocation const& _location);
+	void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, langutil::SourceLocation const& _location);
 
 
 	std::pair<smt::CheckResult, std::vector<std::string>>
@@ -200,8 +205,8 @@ private:
 	/// Used to retrieve models.
 	std::vector<Expression const*> m_uninterpretedTerms;
 	std::vector<smt::Expression> m_pathConditions;
-	ErrorReporter& m_errorReporter;
-	std::shared_ptr<Scanner> m_scanner;
+	langutil::ErrorReporter& m_errorReporter;
+	std::shared_ptr<langutil::Scanner> m_scanner;
 
 	/// Stores the current path of function calls.
 	std::vector<FunctionDefinition const*> m_functionPath;