runtimeverification · dwightguth · May 5, 2023 · Jul 7, 2021 · Jul 7, 2021 · May 5, 2023
diff --git a/k-distribution/k-tutorial/1_basic/commands.sh b/k-distribution/k-tutorial/1_basic/commands.sh
@@ -5,7 +5,7 @@ kompile 02_basics/README.md --md-selector "k & ! exclude" --main-module LESSON-0
 kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-A --syntax-module LESSON-03-A --output-definition build/03a
 kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-B --syntax-module LESSON-03-B --output-definition build/03b
 kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-C --syntax-module LESSON-03-C --output-definition build/03c
-kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-D --syntax-module LESSON-03-D --output-definition build/03d --gen-bison-parser
+kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-D --syntax-module LESSON-03-D --output-definition build/03d
 kompile 04_disambiguation/README.md --md-selector "k & ! exclude" --main-module LESSON-04-A --syntax-module LESSON-04-A --output-definition build/04a
 kompile 04_disambiguation/README.md --md-selector "k & ! exclude" --main-module LESSON-04-B --syntax-module LESSON-04-B --output-definition build/04b
 kompile 04_disambiguation/README.md --md-selector "k & ! exclude" --main-module LESSON-04-C --syntax-module LESSON-04-C --output-definition build/04c

diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile
@@ -1,7 +1,6 @@
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 DEF=lambda
 EXT=lambda
-KOMPILE_FLAGS=--gen-bison-parser
 
 %/arithmetic-div-zero.lambda:
 	true

diff --git a/k-distribution/pl-tutorial/1_k/2_imp/lesson_1/Makefile b/k-distribution/pl-tutorial/1_k/2_imp/lesson_1/Makefile
@@ -1,7 +1,6 @@
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 DEF=imp
 EXT=imp
-KOMPILE_FLAGS=--gen-glr-bison-parser
 
 include $(MAKEFILE_PATH)/../../../find-k.mak
 include ${K_HOME}/include/kframework/ktest.mak
diff --git a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/Makefile b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/Makefile
@@ -1,3 +1,2 @@
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 include $(MAKEFILE_PATH)/../../1_lambda/lesson_1/Makefile
-KOMPILE_FLAGS=--gen-glr-bison-parser
diff --git a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-call-CC-to-callcc/Makefile b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-call-CC-to-callcc/Makefile
@@ -1,3 +1,3 @@
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 include $(MAKEFILE_PATH)/../../Makefile
-KOMPILE_FLAGS=--main-module CALLCC --gen-glr-bison-parser
+KOMPILE_FLAGS=--main-module CALLCC
diff --git a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-callcc-to-call-CC/Makefile b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-callcc-to-call-CC/Makefile
@@ -1,3 +1,3 @@
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 include $(MAKEFILE_PATH)/../callCC/Makefile
-KOMPILE_FLAGS=--main-module CALLCC --syntax-module CALLCC-SYNTAX --gen-glr-bison-parser
+KOMPILE_FLAGS=--main-module CALLCC --syntax-module CALLCC-SYNTAX
diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/Makefile b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/Makefile
@@ -1,7 +1,7 @@
 DEF=imp
 EXT=imp
 KRUN_FLAGS=--output none
-KOMPILE_FLAGS=--gen-glr-bison-parser --enable-search
+KOMPILE_FLAGS=--enable-search
 
 include ../../../find-k.mak
 include ${K_HOME}/include/kframework/ktest.mak

diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/Makefile.concrete b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/Makefile.concrete
@@ -3,7 +3,7 @@ DEF=imp
 DEFDIR=concrete
 KOMPILED=$(DEFDIR)/$(DEF)-kompiled
 EXT=imp
-KOMPILE_FLAGS+=--gen-glr-bison-parser --enable-search
+KOMPILE_FLAGS+=--enable-search
 KRUN_FLAGS=--output none
 
 include $(MAKEFILE_PATH)/../../../find-k.mak

diff --git a/k-distribution/tests/profiling/elrond-semantics/Makefile b/k-distribution/tests/profiling/elrond-semantics/Makefile
@@ -4,6 +4,6 @@ ITER=1
 TESTDIR=.
 KOMPILE_BACKEND=llvm
 BENCHMARK_NAME=ELROND-SEMANTICS
-KOMPILE_FLAGS=--main-module MANDOS --syntax-module MANDOS-SYNTAX
+KOMPILE_FLAGS=--main-module MANDOS --syntax-module MANDOS-SYNTAX --jit-parser
 
 include ../kprofiling.mak
diff --git a/k-distribution/tests/profiling/evm-semantics/Makefile b/k-distribution/tests/profiling/evm-semantics/Makefile
@@ -4,6 +4,6 @@ ITER=1
 TESTDIR=.
 KOMPILE_BACKEND=llvm
 BENCHMARK_NAME=EVM-SEMANTICS
-KOMPILE_FLAGS=--main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION
+KOMPILE_FLAGS=--main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION --jit-parser
 
 include ../kprofiling.mak
diff --git a/k-distribution/tests/profiling/wasm-semantics/Makefile b/k-distribution/tests/profiling/wasm-semantics/Makefile
@@ -4,6 +4,6 @@ ITER=1
 TESTDIR=.
 KOMPILE_BACKEND=llvm
 BENCHMARK_NAME=WASM-SEMANTICS
-KOMPILE_FLAGS=--main-module WASM-TEST --syntax-module WASM-TEST-SYNTAX
+KOMPILE_FLAGS=--main-module WASM-TEST --syntax-module WASM-TEST-SYNTAX --jit-parser
 
 include ../kprofiling.mak
diff --git a/k-distribution/tests/regression-new/amb-rew/Makefile b/k-distribution/tests/regression-new/amb-rew/Makefile
@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=-w2e
+KOMPILE_FLAGS=-w2e -Wno empty-parser
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/append/1.test.kparse.out b/k-distribution/tests/regression-new/append/1.test.kparse.out
@@ -1 +1,2 @@
-\dv{SortInt{}}("1")\dv{SortInt{}}("1")
+\dv{SortInt{}}("1")
+\dv{SortInt{}}("1")
diff --git a/k-distribution/tests/regression-new/bison-glr-bug/Makefile b/k-distribution/tests/regression-new/bison-glr-bug/Makefile
@@ -1,7 +1,6 @@
 DEF=iele
 EXT=
 TESTDIR=.
-KOMPILE_FLAGS+=--gen-glr-bison-parser
 
 test: test.kore
 	cat test.kore | diff - test.ref

diff --git a/k-distribution/tests/regression-new/bison-parser-library/Makefile b/k-distribution/tests/regression-new/bison-parser-library/Makefile
@@ -1,7 +1,7 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--syntax-module TEST --gen-glr-bison-parser --bison-parser-library --llvm-kompile-type c --llvm-kompile-output libfoo
+KOMPILE_FLAGS=--syntax-module TEST --bison-parser-library --llvm-kompile-type c --llvm-kompile-output libfoo
 
 UNAME := $(shell uname)
 ifeq ($(UNAME),Darwin)

diff --git a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k
@@ -1,5 +1,6 @@
 // Copyright (c) K Team. All Rights Reserved.
 module MISSINGKLABEL-SYNTAX
+  syntax KItem ::= "foo" [unused]
 endmodule
 
 module MISSINGKLABEL

diff --git a/k-distribution/tests/regression-new/equals-pattern/Makefile b/k-distribution/tests/regression-new/equals-pattern/Makefile
@@ -2,6 +2,6 @@ DEF=test
 EXT=test
 TESTDIR=.
 KOMPILE_BACKEND?=llvm
-KOMPILE_FLAGS=-w2e
+KOMPILE_FLAGS=-w2e -Wno non-lr-grammar
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/glr/Makefile b/k-distribution/tests/regression-new/glr/Makefile
@@ -1,7 +1,6 @@
 DEF=test
 EXT=foo
 TESTDIR=.
-KOMPILE_FLAGS+=--gen-glr-bison-parser
 
 test: test.kore
 	$(KPRINT) test-kompiled test.kore | diff - test.ref

diff --git a/k-distribution/tests/regression-new/glr2/Makefile b/k-distribution/tests/regression-new/glr2/Makefile
@@ -1,7 +1,6 @@
 DEF=test
 EXT=foo
 TESTDIR=.
-KOMPILE_FLAGS+=--gen-glr-bison-parser
 
 test: test.kore
 	$(KPRINT) test-kompiled test.kore | diff - test.ref

diff --git a/k-distribution/tests/regression-new/glr3/Makefile b/k-distribution/tests/regression-new/glr3/Makefile
@@ -1,7 +1,6 @@
 DEF=test
 EXT=foo
 TESTDIR=.
-KOMPILE_FLAGS+=--gen-glr-bison-parser
 
 test: test.kore
 	$(KPRINT) test-kompiled test.kore | diff - test.ref

diff --git a/k-distribution/tests/regression-new/glr4/Makefile b/k-distribution/tests/regression-new/glr4/Makefile
@@ -1,7 +1,6 @@
 DEF=test
 EXT=foo
 TESTDIR=.
-KOMPILE_FLAGS+=--gen-glr-bison-parser
 
 test: test.kore
 	$(KPRINT) test-kompiled test.kore | diff - test.ref

diff --git a/k-distribution/tests/regression-new/imp++-llvm/Makefile b/k-distribution/tests/regression-new/imp++-llvm/Makefile
@@ -2,7 +2,7 @@ DEF=imp
 EXT=imp
 TESTDIR=.
 KOMPILE_BACKEND=llvm
-KOMPILE_FLAGS=--gen-glr-bison-parser --enable-search
+KOMPILE_FLAGS=--enable-search
 KRUN_FLAGS=--search
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/issue-1384/Makefile b/k-distribution/tests/regression-new/issue-1384/Makefile
@@ -2,6 +2,6 @@ DEF=test
 EXT=test
 TESTDIR=.
 KOMPILE_BACKEND=llvm
-KOMPILE_FLAGS=-w2e
+KOMPILE_FLAGS=-w2e -Wno empty-parser
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/issue-1572/Makefile b/k-distribution/tests/regression-new/issue-1572/Makefile
@@ -1,3 +1,3 @@
-KOMPILE_FLAGS=-w2e -w all --gen-bison-parser
+KOMPILE_FLAGS=-w2e -w all
 
 include ../../../include/kframework/ktest-fail.mak
diff --git a/k-distribution/tests/regression-new/issue-1572/test.k b/k-distribution/tests/regression-new/issue-1572/test.k
@@ -2,6 +2,8 @@
 module TEST-SYNTAX
   imports ML-SYNTAX
 
+  syntax KItem ::= "foo" [unused]
+
 endmodule
 
 module TEST

diff --git a/k-distribution/tests/regression-new/issue-1602/Makefile b/k-distribution/tests/regression-new/issue-1602/Makefile
@@ -1,7 +1,7 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS+=--gen-bison-parser --bison-stack-max-depth 12000
+KOMPILE_FLAGS+=--bison-stack-max-depth 12000
 KRUN_FLAGS=--dry-run --no-expand-macros 1>/dev/null 2>/dev/null
 
 include ../../../include/kframework/ktest.mak

diff --git a/k-distribution/tests/regression-new/llvm-krun/Makefile b/k-distribution/tests/regression-new/llvm-krun/Makefile
@@ -1,6 +1,5 @@
 DEF=test
 KOMPILE_BACKEND=llvm
-KOMPILE_FLAGS+=--gen-glr-bison-parser
 
 CHECK=| diff - test.out
 LLVM_KRUN_FLAGS=-p -d ./test-kompiled

diff --git a/k-distribution/tests/regression-new/locations/Makefile b/k-distribution/tests/regression-new/locations/Makefile
@@ -1,7 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--gen-bison-parser
 KRUN_FLAGS=-o kore
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/locations2/Makefile b/k-distribution/tests/regression-new/locations2/Makefile
@@ -1,7 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--gen-bison-parser
 KRUN_FLAGS=-o kore
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/locations3/Makefile b/k-distribution/tests/regression-new/locations3/Makefile
@@ -1,7 +1,7 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--gen-bison-parser --bison-lists
+KOMPILE_FLAGS=--bison-lists
 KRUN_FLAGS=-o kore
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/nonexhaustive/Makefile b/k-distribution/tests/regression-new/nonexhaustive/Makefile
@@ -1,4 +1,4 @@
-KOMPILE_FLAGS=-w2e -w all -Wno useless-rule
+KOMPILE_FLAGS=-w2e -w all -Wno useless-rule -Wno empty-parser
 KOMPILE_BACKEND=llvm
 
 include ../../../include/kframework/ktest-fail.mak
diff --git a/k-distribution/tests/regression-new/parse-c/Makefile b/k-distribution/tests/regression-new/parse-c/Makefile
@@ -1,7 +1,7 @@
 DEF=c18-translation
 EXT=kc
 TESTDIR=.
-KOMPILE_FLAGS+=--bison-lists --gen-glr-bison-parser
+KOMPILE_FLAGS+=--bison-lists
 test: test.kore
 	$(KPRINT) c18-translation-kompiled test.kore | diff - test.ref
 

diff --git a/k-distribution/tests/regression-new/parseNonPgm/Makefile b/k-distribution/tests/regression-new/parseNonPgm/Makefile
@@ -1,7 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS+=--gen-bison-parser
 KRUN_FLAGS+=print
 
 include ../../../include/kframework/ktest.mak

diff --git a/k-distribution/tests/regression-new/prelude-warnings/Makefile b/k-distribution/tests/regression-new/prelude-warnings/Makefile
@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=-w all -w2e
+KOMPILE_FLAGS=-w all -w2e -Wno empty-parser
 
 include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/werrorCategory/Makefile b/k-distribution/tests/regression-new/werrorCategory/Makefile
@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=-w2e -Wno missing-syntax-module
+KOMPILE_FLAGS=-w2e -Wno missing-syntax-module -Wno non-lr-grammar
 
 include ../../../include/kframework/ktest.mak
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
@@ -32,13 +32,11 @@ public class CheckAtt {
     private final Set<KEMException> errors;
     private final KExceptionManager kem;
     private final Module m;
-    private final boolean isSymbolicKast;
 
-    public CheckAtt(Set<KEMException> errors, KExceptionManager kem, Module m, boolean isSymbolicKast) {
+    public CheckAtt(Set<KEMException> errors, KExceptionManager kem, Module m) {
         this.errors = errors;
         this.kem = kem;
         this.m = m;
-        this.isSymbolicKast = isSymbolicKast;
         this.macros = m.macroKLabels();
     }
 
@@ -95,7 +93,7 @@ private void checkRestrictedAtts(Sentence sentence) {
     private void check(Production prod) {
         if (!prod.sort().equals(Sorts.KItem())) {
             Att sortAtt =  m.sortAttributesFor().getOrElse(prod.sort().head(), () -> Att.empty());
-            if (sortAtt.contains(Att.HOOK()) && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array") && !(sortAtt.get(Att.HOOK()).equals("KVAR.KVar") && isSymbolicKast)) {
+            if (sortAtt.contains(Att.HOOK()) && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array")) {
                 if (!prod.att().contains(Att.FUNCTION()) && !prod.att().contains(Att.BRACKET()) &&
                     !prod.att().contains(Att.TOKEN()) && !prod.att().contains(Att.MACRO()) && !(prod.klabel().isDefined() && macros.contains(prod.klabel().get()))) {
                     if (!(prod.sort().equals(Sorts.K()) && ((prod.klabel().isDefined() && (prod.klabel().get().name().equals("#EmptyK") || prod.klabel().get().name().equals("#KSequence"))) || prod.isSubsort()))) {
@@ -106,7 +104,7 @@ private void check(Production prod) {
                 }
             }
         }
-        if (prod.att().contains(Att.BINDER()) && !isSymbolicKast) {
+        if (prod.att().contains(Att.BINDER())) {
             if (!prod.att().get(Att.BINDER()).equals("")) {
                 errors.add(KEMException.compilerError("Attribute value for 'binder' attribute is not supported.", prod));
             }

diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java b/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java
@@ -24,12 +24,9 @@ public class CheckConfigurationCells {
 
     private final Module module;
 
-    private final boolean isSymbolicKast;
-
-    public CheckConfigurationCells(Set<KEMException> errors, Module module, boolean isSymbolicKast) {
+    public CheckConfigurationCells(Set<KEMException> errors, Module module) {
         this.errors = errors;
         this.module = module;
-        this.isSymbolicKast = isSymbolicKast;
     }
 
     public void check(Sentence s) {
@@ -55,11 +52,9 @@ private void check(Production p) {
                 }
             }
             if (p.att().getOptional(Att.MULTIPLICITY()).orElse("").equals("*") && p.att().getOptional(Att.TYPE()).orElse("Bag").equals("Bag")) {
-                if (!isSymbolicKast) {
-                    errors.add(KEMException.compilerError("Cell bags are only supported on the Java backend. If you want "
-                          + "this feature, comment on https://github.com/runtimeverification/k/issues/1419 . As a workaround, you can add the attribute "
-                          + "type=\"Set\" and add a unique identifier to each element in the set.", p));
-                }
+                errors.add(KEMException.compilerError("Cell bags are only supported on the Java backend. If you want "
+                      + "this feature, comment on https://github.com/runtimeverification/k/issues/1419 . As a workaround, you can add the attribute "
+                      + "type=\"Set\" and add a unique identifier to each element in the set.", p));
             }
         }
     }

diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -182,21 +182,15 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String
 
         ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(kompiledDefinition.mainModule());
 
-        boolean isKast = excludedModuleTags.contains(Att.KORE());
-        Sort rootCell;
-        if (isKast) {
-          rootCell = configInfo.getRootCell();
-        } else {
-          rootCell = Sorts.GeneratedTopCell();
-        }
+        Sort rootCell = Sorts.GeneratedTopCell();
         CompiledDefinition def = new CompiledDefinition(kompileOptions, kompileOptions.outerParsing, kompileOptions.innerParsing, globalOptions, parsedDef, kompiledDefinition, files, kem, configInfo.getDefaultCell(rootCell).klabel());
 
-        if (kompileOptions.genBisonParser || kompileOptions.genGlrBisonParser) {
+        if (!kompileOptions.jitParser || kompileOptions.lr1Parser) {
             if (def.configurationVariableDefaultSorts.containsKey("$PGM")) {
                 String filename = getBisonParserFilename(def.programStartSymbol.name(), def.mainSyntaxModuleName());
                 File outputFile = files.resolveKompiled(filename);
                 File linkFile = files.resolveKompiled("parser_PGM");
-                new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(def.programParsingModuleFor(def.mainSyntaxModuleName(), kem).get(), def.programStartSymbol, outputFile, kompileOptions.genGlrBisonParser, kompileOptions.bisonFile, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary);
+                new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(def.programParsingModuleFor(def.mainSyntaxModuleName(), kem).get(), def.programStartSymbol, outputFile, !kompileOptions.lr1Parser, kompileOptions.bisonFile, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary);
                 try {
                     linkFile.delete();
                     Files.createSymbolicLink(linkFile.toPath(), files.resolveKompiled(".").toPath().relativize(outputFile.toPath()));
@@ -222,7 +216,7 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String
                         String filename = getBisonParserFilename(sort.name(), module);
                         File outputFile = files.resolveKompiled(filename);
                         File linkFile = files.resolveKompiled("parser_" + name);
-                        new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(mod.get(), sort, outputFile, kompileOptions.genGlrBisonParser, null, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary);
+                        new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(mod.get(), sort, outputFile, !kompileOptions.lr1Parser, null, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary);
                         try {
                             linkFile.delete();
                             Files.createSymbolicLink(linkFile.toPath(), files.resolveKompiled(".").toPath().relativize(outputFile.toPath()));
@@ -441,17 +435,16 @@ public void proverChecksX(Module specModule, Module mainDefModule) {
     public void structuralChecks(scala.collection.Set<Module> modules, Module mainModule, Option<Module> kModule, Set<Att.Key> excludedModuleTags) {
         checkAnywhereRules(modules);
         boolean isSymbolic = excludedModuleTags.contains(Att.CONCRETE());
-        boolean isKast = excludedModuleTags.contains(Att.KORE());
         CheckRHSVariables checkRHSVariables = new CheckRHSVariables(errors, !isSymbolic, kompileOptions.backend);
         stream(modules).forEach(m -> stream(m.localSentences()).forEach(checkRHSVariables::check));
 
         stream(modules).forEach(m -> {
-            CheckAtt checkAtt = new CheckAtt(errors, kem, m, isSymbolic && isKast);
+            CheckAtt checkAtt = new CheckAtt(errors, kem, m);
             checkAtt.checkUnrecognizedModuleAtts();
             stream(m.localSentences()).forEach(checkAtt::check);
         });
 
-        stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckConfigurationCells(errors, m, isSymbolic && isKast)::check));
+        stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckConfigurationCells(errors, m)::check));
 
         stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckSortTopUniqueness(errors, m)::check));
 
@@ -461,9 +454,7 @@ public void structuralChecks(scala.collection.Set<Module> modules, Module mainMo
 
         stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckHOLE(errors, m)::check));
 
-        if (!(isSymbolic && isKast)) { // if it's not the java backend
-            stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckTokens(errors, m)::check));
-        }
+        stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckTokens(errors, m)::check));
 
         stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckK(errors)::check));