diff --git a/Changelog.md b/Changelog.md
index 9d8a942ae..4ac7a0d26 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -24,6 +24,7 @@ Bugfixes:
  * SMTChecker: Fix display error for negative integers that are one more than powers of two.
  * SMTChecker: Improved readability for large integers that are powers of two or almost powers of two in error messages.
  * SMTChecker: Fix internal error when a public library function is called internally.
+ * SMTChecker: Fix internal error on multiple wrong SMTChecker natspec entries.
 
 
 ### 0.8.17 (2022-09-08)
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 2baedde12..83602ace3 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -1102,14 +1102,18 @@ set<CHC::CHCNatspecOption> CHC::smtNatspecTags(FunctionDefinition const& _functi
 {
 	set<CHC::CHCNatspecOption> options;
 	string smtStr = "custom:smtchecker";
+	bool errorSeen = false;
 	for (auto const& [tag, value]: _function.annotation().docTags)
 		if (tag == smtStr)
 		{
 			string const& content = value.content;
 			if (auto option = natspecOptionFromString(content))
 				options.insert(*option);
-			else
+			else if (!errorSeen)
+			{
+				errorSeen = true;
 				m_errorReporter.warning(3130_error, _function.location(), "Unknown option for \"" + smtStr + "\": \"" + content + "\"");
+			}
 		}
 	return options;
 }
diff --git a/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_multi_errors_1.sol b/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_multi_errors_1.sol
new file mode 100644
index 000000000..a19923c9c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_multi_errors_1.sol
@@ -0,0 +1,10 @@
+contract C {
+    /// @custom:smtchecker b
+    /// @custom:smtchecker
+    /// @custom:smtchecker a b c
+    function f() internal {}
+}
+
+contract D is C {}
+// ----
+// Warning 3130: (106-130): Unknown option for "custom:smtchecker": "b"