diff --git a/kernel/src/test/java/org/kframework/utils/StringUtilTest.java b/kernel/src/test/java/org/kframework/utils/StringUtilTest.java
index e6ba96cc500..11bb2d402d4 100644
--- a/kernel/src/test/java/org/kframework/utils/StringUtilTest.java
+++ b/kernel/src/test/java/org/kframework/utils/StringUtilTest.java
@@ -31,6 +31,11 @@ public void StringUtilUnquote() throws Exception {
         }
     }
 
+    @Test
+    public void decodeKoreString() {
+        Assert.assertEquals(StringUtil.decodeKoreString("'Unds'V'Unds'9"), "_V_9");
+    }
+
     @Test
     public void testBijection() {
         char[] all = new char[256];
diff --git a/kore/src/main/java/org/kframework/utils/StringUtil.java b/kore/src/main/java/org/kframework/utils/StringUtil.java
index 12869c0bd0e..c3c90306f59 100644
--- a/kore/src/main/java/org/kframework/utils/StringUtil.java
+++ b/kore/src/main/java/org/kframework/utils/StringUtil.java
@@ -6,7 +6,9 @@
 import com.beust.jcommander.JCommander;
 
 import java.util.Arrays;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
@@ -630,6 +632,11 @@ public static String escapeKoreKLabel(String value) {
             "Tild",// 7e
             null// 7f
     };
+    private static final Map<String, Character> asciiReadableEncodingDefaultMap = new HashMap<>();
+    static {
+        for (int i = 0; i < asciiReadableEncodingDefault.length; i++)
+            asciiReadableEncodingDefaultMap.put(asciiReadableEncodingDefault[i], (char) i);
+    }
 
     public static void encodeStringToAlphanumeric(StringBuilder sb, String name, String[] asciiReadableEncodingTable, Pattern identChar, String escapeChar) {
         boolean inIdent = true;
@@ -659,13 +666,25 @@ public static void encodeStringToAlphanumeric(StringBuilder sb, String name, Str
     }
 
     public static String decodeKoreString(String encoded) {
-        for (int i = 0; i < asciiReadableEncodingDefault.length; i++) {
-            String encoding = asciiReadableEncodingDefault[i];
-            if (encoding == null) continue;
-            encoding = "'" + encoding + "'";
-            encoded = encoded.replaceAll(encoding, String.valueOf((char) i));
+        boolean quotedState = false;
+        StringBuilder resultedEncoding = new StringBuilder();
+        StringBuilder tempSb = new StringBuilder();
+        for (int i = 0; i < encoded.length(); i++) {
+            if (quotedState) {
+                if (encoded.charAt(i) == '\'') {
+                    quotedState = false;
+                    resultedEncoding.append(asciiReadableEncodingDefaultMap.get(tempSb.toString()));
+                } else
+                    tempSb.append(encoded.charAt(i));
+            } else {
+                if (encoded.charAt(i) == '\'') {
+                    quotedState = true;
+                    tempSb = new StringBuilder();
+                } else
+                    resultedEncoding.append(encoded.charAt(i));
+            }
         }
-        return encoded;
+        return resultedEncoding.toString();
     }
 
     public static String[] splitOneDimensionalAtt(String att) {