search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
44 stars 24 forks source link

LemmaGenerator #3477

Closed wadoon closed 3 months ago

wadoon commented 4 months ago

Description

Please describe your concern in detail!

Reproducible

Is the issue reproducible? Select one of: always, sometimes, random, have not tried, n/a

Steps to reproduce

Describe the steps needed to reproduce the issue.

  1. ...
  2. ...
  3. ...

What is your expected behavior and what was the actual behavior?

[14:40:35.608] ERROR LemmaGenerationAction - java.lang.NullPointerException: Cannot invoke "org.key_project.util.collection.ImmutableSet.isEmpty()" because "set" is null
at org.key_project.util.collection.DefaultImmutableSet.originalUnion(DefaultImmutableSet.java:135)
at org.key_project.util.collection.DefaultImmutableSet.union(DefaultImmutableSet.java:125)
at de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:336)
at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:570)
at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:461)
at de.uka.ilkd.key.taclettranslation.lemma.TacletLoader.getProofEnvForTaclets(TacletLoader.java:109)
at de.uka.ilkd.key.gui.actions.LemmaGenerationAction$ProveUserDefinedTaclets.loadTaclets(LemmaGenerationAction.java:243)