From c27235b2f5db17c465363dd4387d3377e0ca4a68 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 23 Aug 2019 17:33:29 +0200
Subject: [PATCH] [SMTChecker] Adapt division test for Z3 only

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

diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 5e5fbb9c9..3e5a69a3c 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -116,13 +116,15 @@ BOOST_AUTO_TEST_CASE(division)
 				if (a == 0) {
 					return 0;
 				}
+				// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
+				require(a != 0);
 				uint256 c = a * b;
 				require(c / a == b);
 				return c;
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Division by zero");
+	CHECK_SUCCESS_OR_WARNING(text, "might happen");
 	text = R"(
 		contract C {
 			function div(uint256 a, uint256 b) internal pure returns (uint256) {