AssertionError in krun --prove

[daparpon]

Hi! I am trying to apply the verification infrastructure of K 4.0; however, I cannot get it to work properly, and I ignore why. I want to verify a KernelC test program, based in the example append.c but with minimal changes, with a property rule also based in the [func-spec] one that was provided for it. My aim is to discern how the framework works and how I can use it for more complex programs and specifications.

However, when executing krun --prove on them, I get the following error and trace:

concretizing configuration : java.lang.AssertionError at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:69) at org.kframework.definition.BasicModuleTransformer.processModule(transformers.scala:124) at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$3(transformers.scala:84) at scala.collection.mutable.HashMap.getOrElseUpdate(HashMap.scala:82) at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$2(transformers.scala:84) at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66) at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:84) at org.kframework.definition.SelectiveDefinitionTransformer.apply(transformers.scala:223) at org.kframework.definition.DefinitionTransformer.apply(transformers.scala:202) at org.kframework.frontend.compile.ConcretizeCells.transformDefinition(ConcretizeCells.java:46) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at org.kframework.backend.java.symbolic.JavaBackend.lambda$stepsForProverRules$1(JavaBackend.java:140) at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:80) at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:52) at org.kframework.krun.KRun.run(KRun.java:104) at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:67) at org.kframework.main.FrontEnd.main(FrontEnd.java:34) at org.kframework.main.Main.runApplication(Main.java:415) at org.kframework.main.Main.runApplication(Main.java:264) at org.kframework.main.Main.main(Main.java:73) Caused by: java.lang.AssertionError at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:309) at org.kframework.frontend.KVisitor.apply(transformers.scala:73) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:311) at org.kframework.frontend.KVisitor.apply(transformers.scala:73) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.compile.SortCells.analyzeVars(SortCells.java:322) at org.kframework.frontend.compile.SortCells.sortCells(SortCells.java:82) at org.kframework.frontend.compile.SortCells.sortCells(SortCells.java:110) at org.kframework.frontend.compile.ConcretizeCells.concretize(ConcretizeCells.java:66) at org.kframework.definition.DefinitionTransformer$.$anonfun$fromSentenceTransformer$1(transformers.scala:172) at org.kframework.definition.ModuleTransformer$$anon$1.process(transformers.scala:18) at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:137) at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:135) at org.kframework.definition.SentenceBasedModuleTransformer.$anonfun$process$1(transformers.scala:145) at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234) at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320) at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976) at scala.collection.TraversableLike.map(TraversableLike.scala:234) at scala.collection.TraversableLike.map$(TraversableLike.scala:227) at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47) at scala.collection.SetLike.map(SetLike.scala:101) at scala.collection.SetLike.map$(SetLike.scala:101) at scala.collection.AbstractSet.map(Set.scala:47) at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:142) at org.kframework.definition.BasicModuleTransformer.$anonfun$processModule$1(transformers.scala:124) at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66) ... 28 more concretizing configuration : java.lang.AssertionError at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:69) at org.kframework.definition.BasicModuleTransformer.processModule(transformers.scala:124) at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$3(transformers.scala:84) at scala.collection.mutable.HashMap.getOrElseUpdate(HashMap.scala:82) at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$2(transformers.scala:84) at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66) at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:84) at org.kframework.definition.SelectiveDefinitionTransformer.apply(transformers.scala:223) at org.kframework.definition.DefinitionTransformer.apply(transformers.scala:202) at org.kframework.frontend.compile.ConcretizeCells.transformDefinition(ConcretizeCells.java:46) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at scala.Function1.$anonfun$andThen$1(Function1.scala:52) at org.kframework.backend.java.symbolic.JavaBackend.lambda$stepsForProverRules$1(JavaBackend.java:140) at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:80) at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:52) at org.kframework.krun.KRun.run(KRun.java:104) at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:67) at org.kframework.main.FrontEnd.main(FrontEnd.java:34) at org.kframework.main.Main.runApplication(Main.java:415) at org.kframework.main.Main.runApplication(Main.java:264) at org.kframework.main.Main.main(Main.java:73) Caused by: java.lang.AssertionError at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:309) at org.kframework.frontend.KVisitor.apply(transformers.scala:73) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:311) at org.kframework.frontend.KVisitor.apply(transformers.scala:73) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.KVisitor.$anonfun$apply$5(transformers.scala:86) at java.lang.Iterable.forEach(Iterable.java:75) at org.kframework.frontend.KVisitor.apply(transformers.scala:86) at org.kframework.frontend.compile.SortCells$1.apply(SortCells.java:261) at org.kframework.frontend.KVisitor.apply(transformers.scala:72) at org.kframework.frontend.compile.SortCells.analyzeVars(SortCells.java:322) at org.kframework.frontend.compile.SortCells.sortCells(SortCells.java:82) at org.kframework.frontend.compile.SortCells.sortCells(SortCells.java:110) at org.kframework.frontend.compile.ConcretizeCells.concretize(ConcretizeCells.java:66) at org.kframework.definition.DefinitionTransformer$.$anonfun$fromSentenceTransformer$1(transformers.scala:172) at org.kframework.definition.ModuleTransformer$$anon$1.process(transformers.scala:18) at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:137) at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:135) at org.kframework.definition.SentenceBasedModuleTransformer.$anonfun$process$1(transformers.scala:145) at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234) at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320) at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976) at scala.collection.TraversableLike.map(TraversableLike.scala:234) at scala.collection.TraversableLike.map$(TraversableLike.scala:227) at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47) at scala.collection.SetLike.map(SetLike.scala:101) at scala.collection.SetLike.map$(SetLike.scala:101) at scala.collection.AbstractSet.map(Set.scala:47) at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:142) at org.kframework.definition.BasicModuleTransformer.$anonfun$processModule$1(transformers.scala:124) at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66) ... 28 more [Error] Internal: Uncaught exception thrown of type ModuleTransformerException. 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

What could this error mean, and how could I solve it? I attach both the code file and the specification file (in .txt) in case they are necessary.

Thanks in advance!

insert_spec.txt
insert.txt