From aaaa92012cdab9c11984dfab2d0d56a1c537a61e Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 26 Nov 2018 11:55:53 +0100
Subject: [PATCH] [SMTChecker] Unknown answer for constant condition check
 should not do anything

---
 libsolidity/formal/SMTChecker.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 5b7807f7e..477568a0a 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -889,6 +889,10 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 	{
 		// everything fine.
 	}
+	else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN)
+	{
+		// can't do anything.
+	}
 	else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
 		m_errorReporter.warning(_condition.location(), "Condition unreachable.");
 	else