K-user mailing list

[璟临天下 <qjq793437528 AT 163.com>]

Hello

When i run a program with statement "X = Y" ( "X = 100" can be executed correctly), there is a uncaught exception thrown of type AssertionError. I don't know the reason for this error and how to fix it.

And i rerun it with --debug, the stack trace like below:

java.lang.AssertionError
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.<init>(ConjunctiveFormula.java:98)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.add(ConjunctiveFormula.java:213)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.add(ConjunctiveFormula.java:250)
    at org.kframework.backend.java.builtins.TermEquality.getEqualityTruthValue(TermEquality.java:53)
    at org.kframework.backend.java.builtins.TermEquality.eq(TermEquality.java:22)
    at java.lang.invoke.MethodHandle.invokeWithArguments(MethodHandle.java:627)
    at org.kframework.backend.java.symbolic.BuiltinFunction.invoke(BuiltinFunction.java:105)
    at org.kframework.backend.java.kil.KItem$KItemOperations.evaluateFunction(KItem.java:410)
    at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:334)
    at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:280)
    at org.kframework.backend.java.util.RewriteEngineUtils.construct(RewriteEngineUtils.java:291)
    at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:143)
    at org.kframework.backend.java.util.RewriteEngineUtils.lambda$evaluateConditions$0(RewriteEngineUtils.java:185)
    at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
    at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1382)
    at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
    at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
    at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
    at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
    at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
    at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:187)
    at org.kframework.backend.java.symbolic.PatternMatcher.match(PatternMatcher.java:118)
    at org.kframework.backend.java.kil.KItem.applyAnywhereRules(KItem.java:614)
    at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:334)
    at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:280)
    at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:103)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:719)
    at org.kframework.backend.java.kil.Term.substituteAndEvaluate(Term.java:81)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:363)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:331)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.addAndSimplify(ConjunctiveFormula.java:149)
    at org.kframework.backend.java.kil.ConstrainedTerm.lambda$evaluateConstraints$0(ConstrainedTerm.java:208)
    at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
    at java.util.Iterator.forEachRemaining(Iterator.java:116)
    at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1801)
    at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
    at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
    at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
    at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
    at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
    at org.kframework.backend.java.kil.ConstrainedTerm.evaluateConstraints(ConstrainedTerm.java:216)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:111)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:154)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:95)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:82)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:168)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
    at org.kframework.krun.KRun.run(KRun.java:99)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:90)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:114)
    at org.kframework.main.Main.runApplication(Main.java:104)
    at org.kframework.main.Main.main(Main.java:53)
java.lang.AssertionError
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.<init>(ConjunctiveFormula.java:98)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.add(ConjunctiveFormula.java:213)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.add(ConjunctiveFormula.java:250)
    at org.kframework.backend.java.builtins.TermEquality.getEqualityTruthValue(TermEquality.java:53)
    at org.kframework.backend.java.builtins.TermEquality.eq(TermEquality.java:22)
    at java.lang.invoke.MethodHandle.invokeWithArguments(MethodHandle.java:627)
    at org.kframework.backend.java.symbolic.BuiltinFunction.invoke(BuiltinFunction.java:105)
    at org.kframework.backend.java.kil.KItem$KItemOperations.evaluateFunction(KItem.java:410)
    at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:334)
    at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:280)
    at org.kframework.backend.java.util.RewriteEngineUtils.construct(RewriteEngineUtils.java:291)
    at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:143)
    at org.kframework.backend.java.util.RewriteEngineUtils.lambda$evaluateConditions$0(RewriteEngineUtils.java:185)
    at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
    at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1382)
    at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
    at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
    at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
    at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
    at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
    at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:187)
    at org.kframework.backend.java.symbolic.PatternMatcher.match(PatternMatcher.java:118)
    at org.kframework.backend.java.kil.KItem.applyAnywhereRules(KItem.java:614)
    at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:334)
    at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:280)
    at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:103)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:719)
    at org.kframework.backend.java.kil.Term.substituteAndEvaluate(Term.java:81)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:363)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:331)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.addAndSimplify(ConjunctiveFormula.java:149)
    at org.kframework.backend.java.kil.ConstrainedTerm.lambda$evaluateConstraints$0(ConstrainedTerm.java:208)
    at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
    at java.util.Iterator.forEachRemaining(Iterator.java:116)
    at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1801)
    at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
    at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
    at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
    at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
    at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
    at org.kframework.backend.java.kil.ConstrainedTerm.evaluateConstraints(ConstrainedTerm.java:216)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:111)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:154)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:95)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:82)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:168)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
    at org.kframework.krun.KRun.run(KRun.java:99)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:90)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:114)
    at org.kframework.main.Main.runApplication(Main.java:104)
    at org.kframework.main.Main.main(Main.java:53)
[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 (null)

Thanks for your reading and help.