diff --git a/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
index 670f960b28a..2ed1e40787d 100644
--- a/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
+++ b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -32,6 +32,7 @@
 import org.kframework.builtin.KLabels;
 import org.kframework.builtin.Sorts;
 import org.kframework.compile.AddSortInjections;
+import org.kframework.compile.ComputeTransitiveFunctionDependencies;
 import org.kframework.compile.ExpandMacros;
 import org.kframework.compile.RefreshRules;
 import org.kframework.compile.RewriteToTop;
@@ -107,6 +108,7 @@ public enum SentenceType {
   public static final String ONE_PATH_OP = KLabels.RL_wEF.name();
   public static final String ALL_PATH_OP = KLabels.RL_wAF.name();
   private final Module module;
+  private final Set<String> impureFunctions = new HashSet<>();
   private final AddSortInjections addSortInjections;
   private final KLabel topCellInitializer;
   private final Set<String> mlBinders = new HashSet<>();
@@ -232,6 +234,14 @@ public void convert(
         }
       }
     }
+    ComputeTransitiveFunctionDependencies deps = new ComputeTransitiveFunctionDependencies(module);
+    Set<KLabel> impurities =
+        stream(module.sortedProductions())
+            .filter(prod -> prod.klabel().isDefined() && prod.att().contains(Att.IMPURE()))
+            .filter(prod -> prod.att().contains(Att.IMPURE()))
+            .map(prod -> prod.klabel().get())
+            .collect(Collectors.toSet());
+    impurities.addAll(deps.ancestors(impurities));
 
     semantics.append("\n// symbols\n");
     Set<Production> overloads = new HashSet<>();
@@ -240,8 +250,8 @@ public void convert(
     }
 
     syntax.append(semantics);
-    translateSymbols(attributes, functionRules, overloads, semantics, false);
-    translateSymbols(attributes, functionRules, overloads, syntax, true);
+    translateSymbols(attributes, functionRules, impurities, overloads, semantics, false);
+    translateSymbols(attributes, functionRules, impurities, overloads, syntax, true);
 
     // print syntax definition
     for (Tuple2<Sort, scala.collection.immutable.List<Production>> sort :
@@ -250,6 +260,7 @@ public void convert(
         translateSymbol(
             attributes,
             functionRules,
+            impurities,
             overloads,
             prod.att().get(Att.BRACKET_LABEL(), KLabel.class),
             prod,
@@ -303,8 +314,8 @@ public void convert(
       if (isFunctional(prod)) {
         genFunctionalAxiom(prod, semantics);
       }
-      if (isConstructor(prod, functionRules)) {
-        genNoConfusionAxioms(prod, noConfusion, functionRules, semantics);
+      if (isConstructor(prod, functionRules, impurities)) {
+        genNoConfusionAxioms(prod, noConfusion, functionRules, impurities, semantics);
       }
     }
 
@@ -439,6 +450,7 @@ private void translateSorts(
   private void translateSymbols(
       Map<Att.Key, Boolean> attributes,
       SetMultimap<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
       Set<Production> overloads,
       StringBuilder sb,
       boolean withSyntaxAtts) {
@@ -449,14 +461,25 @@ private void translateSymbols(
       if (prod.klabel().isEmpty()) {
         continue;
       }
+      if (impurities.contains(prod.klabel().get())) {
+        impureFunctions.add(prod.klabel().get().name());
+      }
       translateSymbol(
-          attributes, functionRules, overloads, prod.klabel().get(), prod, sb, withSyntaxAtts);
+          attributes,
+          functionRules,
+          impurities,
+          overloads,
+          prod.klabel().get(),
+          prod,
+          sb,
+          withSyntaxAtts);
     }
   }
 
   private void translateSymbol(
       Map<Att.Key, Boolean> attributes,
       SetMultimap<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
       Set<Production> overloads,
       KLabel label,
       Production prod,
@@ -480,7 +503,7 @@ private void translateSymbol(
     sb.append(") : ");
     convert(prod.sort(), prod, sb);
     sb.append(" ");
-    Att koreAtt = koreAttributes(prod, functionRules, overloads, withSyntaxAtts);
+    Att koreAtt = koreAttributes(prod, functionRules, impurities, overloads, withSyntaxAtts);
     convert(attributes, koreAtt, sb, null, null);
     sb.append("\n");
   }
@@ -714,6 +737,7 @@ private void genNoConfusionAxioms(
       Production prod,
       Set<Tuple2<Production, Production>> noConfusion,
       SetMultimap<KLabel, Rule> functionRulesMap,
+      Set<KLabel> impurities,
       StringBuilder sb) {
     // c(x1,x2,...) /\ c(y1,y2,...) -> c(x1/\y2,x2/\y2,...)
     if (prod.arity() > 0) {
@@ -753,7 +777,7 @@ private void genNoConfusionAxioms(
       if (prod2.klabel().isEmpty()
           || noConfusion.contains(Tuple2.apply(prod, prod2))
           || prod.equals(prod2)
-          || !isConstructor(prod2, functionRulesMap)
+          || !isConstructor(prod2, functionRulesMap, impurities)
           || isBuiltinProduction(prod2)) {
         // TODO (traiansf): add no confusion axioms for constructor vs inj.
         continue;
@@ -1615,8 +1639,9 @@ private void convertParams(Option<KLabel> maybeKLabel, boolean hasR, StringBuild
     sb.append("}");
   }
 
-  private boolean isConstructor(Production prod, SetMultimap<KLabel, Rule> functionRules) {
-    Att att = semanticAttributes(prod, functionRules, java.util.Collections.emptySet());
+  private boolean isConstructor(
+      Production prod, SetMultimap<KLabel, Rule> functionRules, Set<KLabel> impurities) {
+    Att att = semanticAttributes(prod, functionRules, impurities, java.util.Collections.emptySet());
     return att.contains(Att.CONSTRUCTOR());
   }
 
@@ -1652,6 +1677,7 @@ private boolean isGeneratedInKeysOp(Production prod) {
   private Att koreAttributes(
       Production prod,
       SetMultimap<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
       Set<Production> overloads,
       boolean withSyntaxAtts) {
     Att att = prod.att();
@@ -1669,7 +1695,7 @@ private Att koreAttributes(
     for (Att.Key key : attsToRemove) {
       att = att.remove(key);
     }
-    att = att.addAll(semanticAttributes(prod, functionRules, overloads));
+    att = att.addAll(semanticAttributes(prod, functionRules, impurities, overloads));
     if (withSyntaxAtts) {
       att = att.addAll(syntaxAttributes(prod));
     }
@@ -1677,7 +1703,10 @@ private Att koreAttributes(
   }
 
   private Att semanticAttributes(
-      Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {
+      Production prod,
+      SetMultimap<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
+      Set<Production> overloads) {
     boolean isConstructor = !isFunction(prod);
     isConstructor &= !prod.att().contains(Att.ASSOC());
     isConstructor &= !prod.att().contains(Att.COMM());
@@ -1692,16 +1721,20 @@ private Att semanticAttributes(
     boolean isMacro = prod.isMacro();
     boolean isAnywhere = overloads.contains(prod);
 
+    Att att = Att.empty();
+
     if (prod.klabel().isDefined()) {
       for (Rule r : functionRules.get(prod.klabel().get())) {
         isAnywhere |= r.att().contains(Att.ANYWHERE());
       }
+      if (impurities.contains(prod.klabel().get())) {
+        att = att.add(Att.IMPURE());
+      }
     }
 
     isConstructor &= !isMacro;
     isConstructor &= !isAnywhere;
 
-    Att att = Att.empty();
     if (isHook(prod)) {
       att = att.add(Att.HOOK(), prod.att().get(att.HOOK()));
     }
diff --git a/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java b/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
index fe77e3010db..4d758313e59 100644
--- a/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
+++ b/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
@@ -88,10 +88,12 @@ private static <V> Set<V> ancestors(
     while (!queue.isEmpty()) {
       V v = queue.poll();
       Collection<V> neighbors = graph.getPredecessors(v);
-      for (V n : neighbors) {
-        if (!visited.contains(n)) {
-          queue.offer(n);
-          visited.add(n);
+      if (neighbors != null) {
+        for (V n : neighbors) {
+          if (!visited.contains(n)) {
+            queue.offer(n);
+            visited.add(n);
+          }
         }
       }
     }
diff --git a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala
index e81750f1694..040ebcc6265 100644
--- a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala
+++ b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala
@@ -289,7 +289,7 @@ object Att {
   final val IDEM =
     Key.builtin("idem", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
   final val IMPURE =
-    Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+    Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
   final val INDEX =
     Key.builtin("index", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
   final val INITIAL =