diff --git a/tests/lean/bad_set_option.lean b/tests/lean/bad_set_option.lean
new file mode 100644
index 000000000..b65e02362
--- /dev/null
+++ b/tests/lean/bad_set_option.lean
@@ -0,0 +1,3 @@
+set_option boo true
+
+set_option pp.unicode a
diff --git a/tests/lean/bad_set_option.lean.expected.out b/tests/lean/bad_set_option.lean.expected.out
new file mode 100644
index 000000000..78ce16f5d
--- /dev/null
+++ b/tests/lean/bad_set_option.lean.expected.out
@@ -0,0 +1,2 @@
+bad_set_option.lean:1:11: error: unknown option 'boo', type 'help options.' for list of available options
+bad_set_option.lean:3:22: error: invalid Boolean option value, 'true' or 'false' expected