From 955b97097c698ec1808d5688eb3f218e568f6a8f Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 9 Aug 2019 17:49:54 +0200
Subject: [PATCH] [SMTChecker] Relax expectations for complex nonlinear tests

---
 test/libsolidity/AnalysisFramework.h | 13 +++++++++++++
 test/libsolidity/SMTChecker.cpp      |  2 +-
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/test/libsolidity/AnalysisFramework.h b/test/libsolidity/AnalysisFramework.h
index 3fcb9e74a..8eae8c125 100644
--- a/test/libsolidity/AnalysisFramework.h
+++ b/test/libsolidity/AnalysisFramework.h
@@ -153,6 +153,19 @@ do \
 } \
 while(0)
 
+#define CHECK_SUCCESS_OR_WARNING(text, substring) \
+do \
+{ \
+	auto sourceAndError = parseAnalyseAndReturnError((text), true); \
+	auto const& errors = sourceAndError.second; \
+	if (!errors.empty()) \
+	{ \
+		auto message = searchErrors(errors, {{(Error::Type::Warning), (substring)}}); \
+		BOOST_CHECK_MESSAGE(message.empty(), message); \
+	} \
+} \
+while(0)
+
 }
 }
 }
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 88a632f7e..5e5fbb9c9 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -109,7 +109,7 @@ BOOST_AUTO_TEST_CASE(division)
 			}
 		}
 	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
+	CHECK_SUCCESS_OR_WARNING(text, "might happen");
 	text = R"(
 		contract C {
 			function mul(uint256 a, uint256 b) internal pure returns (uint256) {