diff --git a/Changelog.md b/Changelog.md
index 829ea903d..616684d4a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -13,6 +13,7 @@ Compiler Features:
  * ABI Decoder: Raise a runtime error on dirty inputs when using the experimental decoder.
  * SMTChecker: Support arithmetic compound assignment operators.
  * SMTChecker: Support unary increment and decrement for array and mapping access.
+ * SMTChecker: Show unsupported warning for inline assembly blocks.
  * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople.
  * Optimizer: Add rule to simplify certain ANDs and SHL combinations
  * Yul: Adds break and continue keywords to for-loop syntax.
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 7d2a8c8bb..3a3f6323a 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -192,6 +192,15 @@ void SMTChecker::endVisit(FunctionDefinition const&)
 	m_modifierDepthStack.pop_back();
 }
 
+bool SMTChecker::visit(InlineAssembly const& _inlineAsm)
+{
+	m_errorReporter.warning(
+		_inlineAsm.location(),
+		"Assertion checker does not support inline assembly."
+	);
+	return false;
+}
+
 bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index e47bd851c..246f893ac 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -87,6 +87,7 @@ private:
 	void endVisit(Return const& _node) override;
 	bool visit(MemberAccess const& _node) override;
 	void endVisit(IndexAccess const& _node) override;
+	bool visit(InlineAssembly const& _node) override;
 
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.
diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol b/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol
new file mode 100644
index 000000000..a0a07d85e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		assembly {
+		}
+	}
+}
+// ----
+// Warning: (76-93): Assertion checker does not support inline assembly.
diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol b/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol
new file mode 100644
index 000000000..964f357f8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure returns (uint) {
+		assembly {
+			x := 2
+		}
+		return x;
+	}
+}
+// ----
+// Warning: (97-130): Assertion checker does not support inline assembly.