From 0eb067ae4fec6af4faa2a73bdbf2f36b93bd54e0 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 20 May 2020 12:55:12 +0200
Subject: [PATCH] Add SMTLogicError exception catches

---
 libsolidity/interface/StandardCompiler.cpp | 11 +++++++++++
 solc/CommandLineInterface.cpp              | 10 ++++++++++
 2 files changed, 21 insertions(+)

diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 6cf13c309..feda8fc53 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -28,6 +28,7 @@
 #include <libyul/optimiser/Suite.h>
 #include <liblangutil/SourceReferenceFormatter.h>
 #include <libevmasm/Instruction.h>
+#include <libsmtutil/Exceptions.h>
 #include <libsolutil/JSON.h>
 #include <libsolutil/Keccak256.h>
 #include <libsolutil/CommonData.h>
@@ -921,6 +922,16 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 			"Yul exception"
 		));
 	}
+	catch (smtutil::SMTLogicError const& _exception)
+	{
+		errors.append(formatErrorWithException(
+			_exception,
+			false,
+			"SMTLogicException",
+			"general",
+			"SMT logic exception"
+		));
+	}
 	catch (util::Exception const& _exception)
 	{
 		errors.append(formatError(
diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp
index 1342ef1f6..cd792d9c0 100644
--- a/solc/CommandLineInterface.cpp
+++ b/solc/CommandLineInterface.cpp
@@ -47,6 +47,8 @@
 #include <liblangutil/SourceReferenceFormatter.h>
 #include <liblangutil/SourceReferenceFormatterHuman.h>
 
+#include <libsmtutil/Exceptions.h>
+
 #include <libsolutil/Common.h>
 #include <libsolutil/CommonData.h>
 #include <libsolutil/CommonIO.h>
@@ -1295,6 +1297,14 @@ bool CommandLineInterface::processInput()
 			boost::diagnostic_information(_exception);
 		return false;
 	}
+	catch (smtutil::SMTLogicError const& _exception)
+	{
+		serr() <<
+			"SMT logic error during analysis:" <<
+			endl <<
+			boost::diagnostic_information(_exception);
+		return false;
+	}
 	catch (Error const& _error)
 	{
 		if (_error.type() == Error::Type::DocstringParsingError)