diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 7e87e0903..a5f782b42 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -40,6 +40,9 @@ add_test(NAME "lean_eqn_macro"
 add_test(NAME "lean_print_notation"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "print_tests.lean")
+add_test(NAME "auto_completion_issue_422"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./ac_bug.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/tests/lean/extra/ac_bug.sh b/tests/lean/extra/ac_bug.sh
new file mode 100755
index 000000000..aecc6c5d2
--- /dev/null
+++ b/tests/lean/extra/ac_bug.sh
@@ -0,0 +1,19 @@
+#!/bin/sh
+# Regression test for issue https://github.com/leanprover/lean/issues/422
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: ac_bug.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export LEAN_PATH=../../../library:.
+for f in `ls ac_bug*.input`; do
+    echo "testing $f..."
+    $LEAN --server-trace $f > $f.produced.out
+    if grep "nat.mul.assoc" $f.produced.out; then
+        echo "FAILED"
+        exit 1
+    fi
+    rm -f $f.produced.out
+done
+echo "done"
diff --git a/tests/lean/extra/ac_bug1.input b/tests/lean/extra/ac_bug1.input
new file mode 100644
index 000000000..15faa9dab
--- /dev/null
+++ b/tests/lean/extra/ac_bug1.input
@@ -0,0 +1,9 @@
+VISIT ac_bug.lean
+SYNC 4
+import data.nat
+namespace nat
+check mul.as
+exit
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug2.input b/tests/lean/extra/ac_bug2.input
new file mode 100644
index 000000000..83f1e944c
--- /dev/null
+++ b/tests/lean/extra/ac_bug2.input
@@ -0,0 +1,9 @@
+VISIT ac_bug.lean
+SYNC 4
+import data.nat
+namespace nat
+check mul.as
+end nat
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug3.input b/tests/lean/extra/ac_bug3.input
new file mode 100644
index 000000000..6ab990690
--- /dev/null
+++ b/tests/lean/extra/ac_bug3.input
@@ -0,0 +1,10 @@
+VISIT ac_bug.lean
+SYNC 5
+import data.nat
+namespace nat
+check mul.as
+end
+nat
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug4.input b/tests/lean/extra/ac_bug4.input
new file mode 100644
index 000000000..1a513b7f2
--- /dev/null
+++ b/tests/lean/extra/ac_bug4.input
@@ -0,0 +1,10 @@
+VISIT ac_bug.lean
+SYNC 5
+import data.nat
+namespace nat
+check mul.as
+def a := 10
+end nat
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug5.input b/tests/lean/extra/ac_bug5.input
new file mode 100644
index 000000000..3ec26dcfe
--- /dev/null
+++ b/tests/lean/extra/ac_bug5.input
@@ -0,0 +1,9 @@
+VISIT ac_bug.lean
+SYNC 4
+import data.nat
+namespace nat
+check mul.as
+def a := 10
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug6.input b/tests/lean/extra/ac_bug6.input
new file mode 100644
index 000000000..8495814ae
--- /dev/null
+++ b/tests/lean/extra/ac_bug6.input
@@ -0,0 +1,10 @@
+VISIT ac_bug.lean
+SYNC 5
+import data.nat
+namespace nat
+check mul.as
+def a := 10
+exit
+WAIT
+FINDP 3
+mul.as