1 files changed, 40 insertions, 0 deletions
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index b97fc80e..beb933a4 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -377,6 +377,46 @@ BOOST_AUTO_TEST_CASE(bool_simple)
 		}
 	)";
 	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(bool x) public pure {
+				require(x);
+				bool y;
+				y = false;
+				assert(x || y);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(bool x) public pure {
+				bool y;
+				assert(x <= y);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	text = R"(
+		contract C {
+			function f(bool x) public pure {
+				bool y;
+				assert(x >= y);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(bool x) public pure {
+				require(x);
+				bool y;
+				assert(x > y);
+				assert(y < x);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
 BOOST_AUTO_TEST_CASE(bool_int_mixed)