From 1ece7bf4433a37feb449b7f3b4f820a1f5740eaf Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 6 Jul 2017 11:05:05 +0200
Subject: z3 conditions

---
 libsolidity/interface/CompilerStack.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'libsolidity/interface/CompilerStack.cpp')

diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 412d2fd3..4283cd99 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -37,6 +37,7 @@
 #include <libsolidity/analysis/PostTypeChecker.h>
 #include <libsolidity/analysis/SyntaxChecker.h>
 #include <libsolidity/codegen/Compiler.h>
+#include <libsolidity/formal/SMTChecker.h>
 #include <libsolidity/interface/ABI.h>
 #include <libsolidity/interface/Natspec.h>
 #include <libsolidity/interface/GasEstimator.h>
@@ -236,6 +237,13 @@ bool CompilerStack::analyze()
 				noErrors = false;
 	}
 
+	if (noErrors)
+	{
+		SMTChecker smtChecker(m_errorReporter);
+		for (Source const* source: m_sourceOrder)
+			smtChecker.analyze(*source->ast);
+	}
+
 	if (noErrors)
 	{
 		m_stackState = AnalysisSuccessful;
-- 
cgit v1.2.3


From b3f8ed457a10dab36abaef72310a755a95e0753f Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Tue, 11 Jul 2017 13:26:43 +0200
Subject: Cleanup.

---
 libsolidity/interface/CompilerStack.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'libsolidity/interface/CompilerStack.cpp')

diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 4283cd99..50e20b3d 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -239,7 +239,7 @@ bool CompilerStack::analyze()
 
 	if (noErrors)
 	{
-		SMTChecker smtChecker(m_errorReporter);
+		SMTChecker smtChecker(m_errorReporter, m_readFile);
 		for (Source const* source: m_sourceOrder)
 			smtChecker.analyze(*source->ast);
 	}
-- 
cgit v1.2.3


From 9ac2ac14c1819be2341c6947245bf63b02795528 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 13 Jul 2017 21:06:04 +0200
Subject: Rename read file callback.

---
 libsolidity/interface/CompilerStack.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'libsolidity/interface/CompilerStack.cpp')

diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 50e20b3d..363f45dd 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -239,7 +239,7 @@ bool CompilerStack::analyze()
 
 	if (noErrors)
 	{
-		SMTChecker smtChecker(m_errorReporter, m_readFile);
+		SMTChecker smtChecker(m_errorReporter, m_smtQuery);
 		for (Source const* source: m_sourceOrder)
 			smtChecker.analyze(*source->ast);
 	}
@@ -535,17 +535,17 @@ StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string
 			if (m_sources.count(importPath) || newSources.count(importPath))
 				continue;
 
-			ReadFile::Result result{false, string("File not supplied initially.")};
+			ReadCallback::Result result{false, string("File not supplied initially.")};
 			if (m_readFile)
 				result = m_readFile(importPath);
 
 			if (result.success)
-				newSources[importPath] = result.contentsOrErrorMessage;
+				newSources[importPath] = result.responseOrErrorMessage;
 			else
 			{
 				m_errorReporter.parserError(
 					import->location(),
-					string("Source \"" + importPath + "\" not found: " + result.contentsOrErrorMessage)
+					string("Source \"" + importPath + "\" not found: " + result.responseOrErrorMessage)
 				);
 				continue;
 			}
-- 
cgit v1.2.3