Checked that KT-4453 has been fixed recently by change in TipsManager

idea/testData/completion/basic/common/extensions/NoDuplicatedMethodForSmartCast.kt

@@ -0,0 +1,18 @@
+trait A {
+    fun foo(): Int
+}
+
+trait B: A {
+    override fun foo(): Int
+    override fun foo1(): Int
+}
+
+fun g(a: A) {
+    if (a is B) {
+        a.fo<caret>
+    }
+}
+
+// EXIST: foo
+// EXIST: foo1
+// NUMBER: 2

idea/tests/org/jetbrains/jet/completion/JSBasicCompletionTestGenerated.java

@@ -846,6 +846,12 @@ public class JSBasicCompletionTestGenerated extends AbstractJSBasicCompletionTes
                 doTest(fileName);
             }
 
+            @TestMetadata("NoDuplicatedMethodForSmartCast.kt")
+            public void testNoDuplicatedMethodForSmartCast() throws Exception {
+                String fileName = JetTestUtils.navigationMetadata("idea/testData/completion/basic/common/extensions/NoDuplicatedMethodForSmartCast.kt");
+                doTest(fileName);
+            }
+
             @TestMetadata("WrongExplicitReceiver.kt")
             public void testWrongExplicitReceiver() throws Exception {
                 String fileName = JetTestUtils.navigationMetadata("idea/testData/completion/basic/common/extensions/WrongExplicitReceiver.kt");

idea/tests/org/jetbrains/jet/completion/JvmBasicCompletionTestGenerated.java

@@ -846,6 +846,12 @@ public class JvmBasicCompletionTestGenerated extends AbstractJvmBasicCompletionT
                 doTest(fileName);
             }
 
+            @TestMetadata("NoDuplicatedMethodForSmartCast.kt")
+            public void testNoDuplicatedMethodForSmartCast() throws Exception {
+                String fileName = JetTestUtils.navigationMetadata("idea/testData/completion/basic/common/extensions/NoDuplicatedMethodForSmartCast.kt");
+                doTest(fileName);
+            }
+
             @TestMetadata("WrongExplicitReceiver.kt")
             public void testWrongExplicitReceiver() throws Exception {
                 String fileName = JetTestUtils.navigationMetadata("idea/testData/completion/basic/common/extensions/WrongExplicitReceiver.kt");