diff --git a/k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k b/k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k
new file mode 100644
index 00000000000..b21637e84bf
--- /dev/null
+++ b/k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k
@@ -0,0 +1,13 @@
+module CHECKNOSYMBOLOVERLOAD-SYNTAX
+endmodule
+
+module CHECKNOSYMBOLOVERLOAD
+  syntax LVal
+  syntax RVal
+  syntax Val ::= LVal | RVal
+  syntax Exp ::= Val
+
+  syntax RVals ::= RVal [overload(arg)]
+  syntax Vals  ::= Val  [overload(arg), symbol(val)]
+  syntax Exps  ::= Exp  [overload(arg)]
+endmodule
diff --git a/k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k.out b/k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k.out
new file mode 100644
index 00000000000..67615767feb
--- /dev/null
+++ b/k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k.out
@@ -0,0 +1,11 @@
+[Error] Compiler: Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.
+	Source(checkNoSymbolOverload.k)
+	Location(10,20,10,40)
+	10 |	  syntax RVals ::= RVal [overload(arg)]
+	   .	                   ^~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.
+	Source(checkNoSymbolOverload.k)
+	Location(12,20,12,40)
+	12 |	  syntax Exps  ::= Exp  [overload(arg)]
+	   .	                   ^~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 2 structural errors.
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/Makefile b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/Makefile
new file mode 100644
index 00000000000..86158b0f8d9
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/Makefile
@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test
new file mode 100644
index 00000000000..a9f17866dc6
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test
@@ -0,0 +1 @@
+rv(0), rv(1), rv(2), (1, 2)
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test.out b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test.out
new file mode 100644
index 00000000000..e735208f1ef
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test.out
@@ -0,0 +1,3 @@
+<k>
+  exps ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test
new file mode 100644
index 00000000000..f5faa7fb543
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test
@@ -0,0 +1 @@
+rv(0), rv(1), rv(2)
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test.out b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test.out
new file mode 100644
index 00000000000..929ccbc6026
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test.out
@@ -0,0 +1,3 @@
+<k>
+  rvals ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/test.k b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/test.k
new file mode 100644
index 00000000000..6587cf9cc5a
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/test.k
@@ -0,0 +1,39 @@
+module TEST
+  imports DOMAINS
+
+  syntax LVal ::= lv(Int) | lv(Id)
+  syntax RVal ::= rv(Int)
+  syntax Val  ::= LVal | RVal
+
+  syntax Exp  ::= Int
+                | Id
+                | Val
+                | "(" Exp ")" [bracket]
+                > left:
+                  Exp "," Exp [group(comma)]
+
+  syntax RVals ::= RVal           [overload(arg),  group(assignExp), symbol(rval), avoid]
+                 | RVals "," RVal [overload(exps), group(assignExp)]
+
+  syntax Vals  ::= Val            [overload(arg),  group(assignExp), symbol(val),  avoid]
+                 | Vals "," Val   [overload(exps), group(assignExp)]
+
+  syntax Exps  ::= Exp            [overload(arg),  group(assignExp), symbol(exp),  avoid]
+                 | Exps "," Exp   [overload(exps), group(assignExp)]
+
+  syntax Exps ::= Vals
+  syntax Vals ::= RVals
+
+  syntax priority assignExp > comma
+
+  syntax KItem ::= "rvals"
+                 | "vals"
+                 | "exps"
+
+  configuration
+    <k> $PGM:Exps </k>
+
+  rule _:RVals => rvals
+  rule _:Vals  => vals
+  rule _:Exps  => exps  [owise]
+endmodule
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test
new file mode 100644
index 00000000000..bb34114721f
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test
@@ -0,0 +1 @@
+rv(0), lv(x), rv(2)
diff --git a/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test.out b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test.out
new file mode 100644
index 00000000000..e3ac7ad7c00
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test.out
@@ -0,0 +1,3 @@
+<k>
+  vals ~> .K
+</k>
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
index 8000f08ea89..0bf8af0b12f 100644
--- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
+++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
@@ -73,6 +73,7 @@ private void checkProduction(Production prod) {
     checkSymbolKLabel(prod);
     checkKLabelOverload(prod);
     checkNullarySymbol(prod);
+    checkNoSymbolOverload(prod);
   }
 
   private <T extends HasAtt & HasLocation> void checkUnrecognizedAtts(T term) {
@@ -360,6 +361,15 @@ private void checkKLabelOverload(Production prod) {
     }
   }
 
+  private void checkNoSymbolOverload(Production prod) {
+    if (prod.klabel().isEmpty() && prod.att().contains(Att.OVERLOAD())) {
+      errors.add(
+          KEMException.compilerError(
+              "Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.",
+              prod));
+    }
+  }
+
   private void checkNullarySymbol(Production prod) {
     if (prod.att().contains(Att.SYMBOL()) && !prod.att().contains(Att.KLABEL())) {
       if (prod.att().get(Att.SYMBOL()).isEmpty()) {