I had some rules that had the same identifier at least twice on the left hand side, with the intention that the positions where they appear need to have the same value (I assume that is how it should). It seemed to work for a long time (but this may be because of the lack of rigorous testing). Then one day I got a strange exception (see later). I only could get rid of it by replacing all of the mentioned rules by ones that capture the value with different names and then use a when V1 ==K V2 clause to ensure identity.
java.lang.AssertionError: unimplemented
at org.kframework.utils.OneIntegerGenericBitSet.clear(OneIntegerGenericBitSet.java:183)
at org.kframework.backend.java.symbolic.FastRuleMatcher.addSubstitution(FastRuleMatcher.java:476)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:241)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:247)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:159)
at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:100)
at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:81)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
at org.kframework.krun.KRun.run(KRun.java:86)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:110)
at org.kframework.main.Main.runApplication(Main.java:100)
at org.kframework.main.Main.main(Main.java:52)
java.lang.AssertionError: unimplemented
at org.kframework.utils.OneIntegerGenericBitSet.clear(OneIntegerGenericBitSet.java:183)
at org.kframework.backend.java.symbolic.FastRuleMatcher.addSubstitution(FastRuleMatcher.java:476)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:241)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:247)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:159)
at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:100)
at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:81)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
at org.kframework.krun.KRun.run(KRun.java:86)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:110)
at org.kframework.main.Main.runApplication(Main.java:100)
at org.kframework.main.Main.main(Main.java:52)
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
I had some rules that had the same identifier at least twice on the left hand side, with the intention that the positions where they appear need to have the same value (I assume that is how it should). It seemed to work for a long time (but this may be because of the lack of rigorous testing). Then one day I got a strange exception (see later). I only could get rid of it by replacing all of the mentioned rules by ones that capture the value with different names and then use a when V1 ==K V2 clause to ensure identity.
java.lang.AssertionError: unimplemented at org.kframework.utils.OneIntegerGenericBitSet.clear(OneIntegerGenericBitSet.java:183) at org.kframework.backend.java.symbolic.FastRuleMatcher.addSubstitution(FastRuleMatcher.java:476) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:241) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:247) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107) at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:159) at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:100) at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:81) at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137) at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70) at org.kframework.krun.KRun.run(KRun.java:86) at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97) at org.kframework.main.FrontEnd.main(FrontEnd.java:52) at org.kframework.main.Main.runApplication(Main.java:110) at org.kframework.main.Main.runApplication(Main.java:100) at org.kframework.main.Main.main(Main.java:52) java.lang.AssertionError: unimplemented at org.kframework.utils.OneIntegerGenericBitSet.clear(OneIntegerGenericBitSet.java:183) at org.kframework.backend.java.symbolic.FastRuleMatcher.addSubstitution(FastRuleMatcher.java:476) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:241) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:247) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271) at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315) at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107) at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:159) at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:100) at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:81) at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137) at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70) at org.kframework.krun.KRun.run(KRun.java:86) at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97) at org.kframework.main.FrontEnd.main(FrontEnd.java:52) at org.kframework.main.Main.runApplication(Main.java:110) at org.kframework.main.Main.runApplication(Main.java:100) at org.kframework.main.Main.main(Main.java:52) [Error] Internal: Uncaught exception thrown of type AssertionError. Please rerun your program with the --debug flag to generate a stack trace, and file a bug report at https://github.com/kframework/k/issues