diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 0c083abce..e5c1aef44 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -139,8 +139,13 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 	}
 	else if (arguments.empty())
 	{
-		// We assume it is an integer...
-		return m_context.int_val(n.c_str());
+		if (n == "true")
+			return m_context.bool_val(true);
+		else if (n == "false")
+			return m_context.bool_val(false);
+		else
+			// We assume it is an integer...
+			return m_context.int_val(n.c_str());
 	}
 
 	solAssert(arity.count(n) && arity.at(n) == arguments.size(), "");
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 9d014125e..9fbab03a2 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -362,18 +362,15 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 		}
 	)";
 	CHECK_WARNING(text, "Condition is always false");
-// TODO
-//	// a plain literal constant is fine
-//	text = R"(
-//		contract C {
-//			function f(uint x) public pure {
-//				if (true) { revert(); }
-//			}
-//		}
-//	)";
-//	CHECK_SUCCESS_NO_WARNINGS(text);
-
-// TODO test unreacheable code
+	// a plain literal constant is fine
+	text = R"(
+		contract C {
+			function f(uint) public pure {
+				if (true) { revert(); }
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
 BOOST_AUTO_TEST_SUITE_END()