diff --git a/Changelog.md b/Changelog.md
index f06881e97..ec12a214b 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -29,6 +29,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables.
  * SMTChecker: Fix internal error when short circuiting Boolean expressions with function calls in state variable initialization.
  * SMTChecker: Fix internal error when assigning to index access inside branches.
+ * SMTChecker: Fix internal error on try/catch clauses with parameters.
 
 ### 0.6.8 (2020-05-14)
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 8ed8d71fa..b06abbe6e 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -274,6 +274,20 @@ bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
 	return false;
 }
 
+bool SMTEncoder::visit(TryCatchClause const& _clause)
+{
+	if (auto params = _clause.parameters())
+		for (auto const& var: params->parameters())
+			createVariable(*var);
+
+	m_errorReporter.warning(
+		7645_error,
+		_clause.location(),
+		"Assertion checker does not support try/catch clauses."
+	);
+	return false;
+}
+
 bool SMTEncoder::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 8010ba820..0e4c170fc 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -91,6 +91,7 @@ protected:
 	bool visit(InlineAssembly const& _node) override;
 	void endVisit(Break const&) override {}
 	void endVisit(Continue const&) override {}
+	bool visit(TryCatchClause const& _node) override;
 
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol
new file mode 100644
index 000000000..b41027ed4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() public returns (uint) {
+		try this.g() returns (uint x) { x; }
+		catch Error(string memory s) { s; }
+	}
+}
+// ====
+// EVMVersion: >=byzantium
+// ----
+// Warning: (98-121): Assertion checker does not support try/catch clauses.
+// Warning: (124-159): Assertion checker does not support try/catch clauses.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol
new file mode 100644
index 000000000..96de08886
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public {
+		try this.f() {}
+		catch (bytes memory x) {
+			x;
+		}
+	}
+}
+// ====
+// EVMVersion: >=byzantium
+// ----
+// Warning: (83-85): Assertion checker does not support try/catch clauses.
+// Warning: (88-122): Assertion checker does not support try/catch clauses.