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')

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