Process completed with exit code 1.

`compare()` called on itself

`compareToIgnoreCase()` called on itself

`compare()` called on itself

`compare()` called on itself

'finalize()' should not be overridden

'finalize()' should not be overridden

'finalize()' should not be overridden

`switch (response) { case YES_THIS_INSTANCE -> { // handle this b...` statement on enum type 'de.uka.ilkd.key.smt.newsmt2.SMTHandler.Capability' misses case 'UNABLE'

String values are compared using `==`, not 'equals()'

String values are compared using `!=`, not 'equals()'

String values are compared using `==`, not 'equals()'

String values are compared using `==`, not 'equals()'

String values are compared using `==`, not 'equals()'

Should be one of: InputEvent.SHIFT_MASK, InputEvent.CTRL_MASK, InputEvent.META_MASK, InputEvent.ALT_MASK, ... or their combination

Should be one of: InputEvent.SHIFT_MASK, InputEvent.CTRL_MASK, InputEvent.META_MASK, InputEvent.ALT_MASK, ... or their combination

Should be one of: InputEvent.SHIFT_MASK, InputEvent.CTRL_MASK, InputEvent.META_MASK, InputEvent.ALT_MASK, ... or their combination

Should be one of: JComponent.WHEN_FOCUSED, JComponent.WHEN_IN_FOCUSED_WINDOW, ...

Should be one of: InputEvent.SHIFT_MASK, InputEvent.CTRL_MASK, InputEvent.META_MASK, InputEvent.ALT_MASK, ... or their combination

Should be one of: InputEvent.SHIFT_MASK, InputEvent.CTRL_MASK, InputEvent.META_MASK, InputEvent.ALT_MASK, ... or their combination

Variable 'queue' is not updated inside loop

Source parameter type 'java.lang.Object\[\]' is not assignable to destination parameter `array` of type 'T\[\]'

`dest` is not of an array type

Source parameter type 'S\[\]' is not assignable to destination parameter `result` of type 'T\[\]'

`else` statement has empty body

`else` statement has empty body

`for` statement has empty body

`for` statement has empty body

`if` statement has empty body

`if` statement has empty body

`if` statement has empty body

`else` statement has empty body

`if` statement has empty body

`else` statement has empty body

`if` statement has empty body

`else` statement has empty body

`if` statement has empty body

`else` statement has empty body

`else` statement has empty body

`if` statement has empty body

`if` statement has empty body

`if` statement has empty body

`if` statement has empty body

`if` statement has empty body

`if` statement has empty body

`if` statement has empty body

`if` statement has empty body

`for` statement has empty body

`while` statement has empty body

`if` statement has empty body

`for` statement has empty body

`for` statement has empty body

`if` statement has empty body

`if` statement has empty body

`for` statement has empty body

`if` statement has empty body

`if` statement has empty body

Referencing subclass True from superclass SMTTerm initializer might lead to class loading deadlock

Referencing subclass False from superclass SMTTerm initializer might lead to class loading deadlock

Referencing subclass MergeByIfThenElse from superclass MergeProcedure initializer might lead to class loading deadlock

Referencing subclass NILSequent from superclass Sequent initializer might lead to class loading deadlock

Referencing subclass DivideMonomials from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaMul from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MemberPVToField from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass ArrayBaseInstanceOf from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass CreateLocalAnonUpdate from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass EnumConstantValue from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass ConstantValue from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaBinaryXOr from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaAdd from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaShiftLeft from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaGeq from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaBinaryOr from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaGreater from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass CreateFrameCond from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaEqual from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass CreateHeapAnonUpdate from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaLess from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass CreateBeforeLoopUpdate from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass AddCast from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaBinaryAnd from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass DivideLCRMonomials from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaDiv from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaSub from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass ObserverEqualityMetaConstruct from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaShiftRight from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass ExpandQueriesMetaConstruct from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaLeq from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass CreateWellformedCond from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass IntroAtPreDefsOp from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass MetaPow from superclass AbstractTermTransformer initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionStringSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass NonSimpleMethodReferenceSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass ConstantProgramVariableSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionNonStringObjectSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass ConstantProgramVariableSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass LeftHandSideSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass MethodNameSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSpecialPrimitiveTypeSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass TypeReferenceNotPrimitiveSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass NonSimpleExpressionSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass SimpleExpressionSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass ExpressionSort from superclass ProgramSVSort initializer might lead to class loading deadlock

Referencing subclass JavaProfile from superclass AbstractProfile initializer might lead to class loading deadlock

Referencing subclass TacletFilterTrue from superclass TacletFilter initializer might lead to class loading deadlock

Referencing subclass IntRuleAppCost from superclass NumberRuleAppCost initializer might lead to class loading deadlock

Referencing subclass TopLevelWithUpdate from superclass TopLevelFindFeature initializer might lead to class loading deadlock

Referencing subclass TopLevelWithoutUpdate from superclass TopLevelFindFeature initializer might lead to class loading deadlock

Referencing subclass TopLevelWithoutUpdate from superclass TopLevelFindFeature initializer might lead to class loading deadlock

Referencing subclass TopLevelWithoutUpdate from superclass TopLevelFindFeature initializer might lead to class loading deadlock

Referencing subclass TopLevelWithUpdate from superclass TopLevelFindFeature initializer might lead to class loading deadlock

Referencing subclass TopLevelWithUpdate from superclass TopLevelFindFeature initializer might lead to class loading deadlock

Referencing subclass EmptyOracleLocationSet from superclass OracleLocationSet initializer might lead to class loading deadlock

Referencing subclass AllLocsLocationSet from superclass OracleLocationSet initializer might lead to class loading deadlock

Manual array copy

`assert` has side effects: call to 'getArrayLength()' mutates field 'length'

`assert` has side effects: call to 'subTerm()' mutates field 'subTermCache'

Redundant character escape `\\\"` in RegExp

Redundant character escape `\\}` in RegExp

Obsolete collection type `Hashtable` used

Obsolete collection type `Hashtable<>` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack` used

Obsolete collection type `java.util.Vector` used

Obsolete collection type `java.util.Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Vector` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Stack<>` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack` used

Obsolete collection type `Stack<>` used

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

Method `clone()` does not call 'super.clone()'

`equal()` method should probably be 'equals()'

`equal()` method should probably be 'equals()'

Octal integer `07`

Octal integer `077`

Octal integer `077`

Octal integer `077`

Octal integer `077`

Octal integer `077`

Octal integer `077`

Octal integer `077`

Octal integer `077`

Octal integer `077`

`StringBuilder` can be replaced with 'String'

`StringBuilder sb` can be replaced with 'String'

`StringBuilder sb` can be replaced with 'String'

Method invocation `getName` may produce `NullPointerException`

Condition `prettyName != null` is always `true`

Condition `droppedString != null` is always `true`

Variable is already assigned to this value

Variable is already assigned to this value

Variable is already assigned to this value

Variable is already assigned to this value

Method invocation `name` may produce `NullPointerException`

Condition `a.length == 0` is always `false` when reached

Dereference of `inst` may produce `NullPointerException`

Condition `result == null` is always `false`

Argument `problem` might be null

Method invocation `getLastPathComponent` may produce `NullPointerException`

Method invocation `toString` may produce `NullPointerException`

Condition `applicable` is always `true` when reached

Dereference of `directory.listFiles()` may produce `NullPointerException`

Argument `javaSourceLocation` might be null

Argument `file.orElse(null)` might be null

Condition `source != null` is always `true`

Condition `file.isPresent()` is always `true`

Method invocation `getUserData` may produce `NullPointerException`

Argument `notificationAfterMacro.getSelectedItem()` might be null

Argument `getClass().getResourceAsStream("/fonts/typicons.ttf")` might be null

Argument `getClass().getResourceAsStream("/fonts/Font Awesome 6 Free-Regular-400.otf")` might be null

Argument `Entypo.class.getResourceAsStream("/fonts/entypo.ttf")` might be null

Argument `getClass().getResourceAsStream("/fonts/Font Awesome 6 Brands-Regular-400.otf")` might be null

Argument `getClass().getResourceAsStream("/fonts/MaterialIcons-Regular.ttf")` might be null

Argument `keyHole` might be null

Argument `keyVersionLogo` might be null

Argument `keyHoleAlmostClosed` might be null

Argument `junit` might be null

Argument `keyLogo` might be null

Argument `keyCachedClosed` might be null

Argument `keyVersionLogo` might be null

Argument `keyHoleInteractive` might be null

Argument `jml` might be null

Argument `oneStepSimplifier` might be null

Argument `keyHoleLinked` might be null

Argument `getClass().getResourceAsStream("/fonts/Font Awesome 6 Free-Solid-900.otf")` might be null

Condition `cl.getSuperclass() == null` is always `true` when reached

Method invocation `getServices` may produce `NullPointerException`

Condition `!started` is always `true`

Condition `sourcePos == null` is always `false`

Condition `Match_MaxBits == 0` is always `false`

Condition `Match_Distance == 0` is always `false`

Variable is already assigned to this value

Condition `end > 0` is always `true`

Condition `text != null` is always `true`

Method invocation `setBounds` may produce `NullPointerException`

Argument `old` might be null

Method invocation `getAbsolutePath` may produce `NullPointerException`

Dereference of `jars` may produce `NullPointerException`

Result of `res.size()` is always '0'

Argument `list` might be null

Condition `ref instanceof PackageReference` is always `false`

Variable is already assigned to this value

Method invocation `makeAllParentRolesValid` may produce `NullPointerException`

Method invocation `makeParentRoleValid` may produce `NullPointerException`

Condition `refs != null` is always `true`

Condition `clone != null` is always `true`

Condition `code == PACKAGE` is always `true`

Variable is already assigned to this value

Variable is already assigned to this value

Variable is already assigned to this value

Method invocation `add` may produce `NullPointerException`

Method invocation `getIdentifier` may produce `NullPointerException`

Argument `method.getName()` might be null

Argument `name` might be null

Argument `name` might be null

Argument `name` might be null

Method invocation `equals` may produce `NullPointerException`

Argument `tn` might be null

Method invocation `remove` may produce `NullPointerException`

Method invocation `equals` may produce `NullPointerException`

Method invocation `equals` may produce `NullPointerException`

Condition `stype != null && !btype.equals(stype)` is always `false`

Condition `!btype.equals(stype)` is always `false` when reached

Result of `btype.equals(stype)` is always 'true'

Condition `gtype != null && !btype.equals(gtype)` is always `false`

Condition `!btype.equals(gtype)` is always `false` when reached

Result of `btype.equals(gtype)` is always 'true'

Method invocation `equals` may produce `NullPointerException`

Method invocation `deepClone` may produce `NullPointerException`

Argument `expression` might be null

Method invocation `getClass` may produce `NullPointerException`

Method invocation `equals` may produce `NullPointerException`

Condition `index >= 0` is always `true`

Condition `var instanceof EnumConstantSpecification` is always `false` when reached

Condition `var instanceof EnumConstantSpecification && this instanceof EnumDeclaration` is always `false` when reached

Condition `mods != null` is always `true`

Condition `idx >= -1` is always `true`

Condition `index >= 0` is always `true`

Dereference of `content` may produce `NullPointerException`

Condition `result == null` is always `true`

Condition `result != null` is always `true`

Condition `op instanceof LogicalAnd` is always `false`

Condition `op instanceof LogicalOr` is always `false`

Casting `v` to `Field` may produce `ClassCastException`

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Variable is already assigned to this value

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition is always true

Condition `m instanceof EnumConstantDeclaration` is always `false`

Condition `op instanceof PreIncrement` is always `false`

Condition `op instanceof PostIncrement` is always `false`

Condition `op instanceof PreDecrement` is always `false`

Condition `op instanceof PostDecrement` is always `false`

Argument `trname` might be null

Method invocation `getBody` may produce `NullPointerException`

Condition `pe instanceof UncollatedReferenceQualifier` is always `false`

Condition `pe instanceof EnumConstantSpecification` is always `false`

Method invocation `charAt` may produce `NullPointerException`

Condition `result == null` is always `true`

Casting `scope` to `CompilationUnit` may produce `ClassCastException`

Casting `cur` to `CompilationUnit` may produce `ClassCastException`

Condition `name == null` is always `false`

Variable is already assigned to this value

Condition `typeArgs.length != 0` is always `true`

Variable is already assigned to this value

Method invocation `pos` may produce `NullPointerException`

Method invocation `getJavaInfo` may produce `NullPointerException`

Dereference of `annot` may produce `NullPointerException`

The call to 'assertBoolean' always fails, according to its method contracts

Casting `object` to `Term` may produce `ClassCastException`

Casting `object` to `Term` may produce `ClassCastException`

Casting `o` to `Term` may produce `ClassCastException`

Method invocation `charAt` may produce `NullPointerException`

Method invocation `charAt` may produce `NullPointerException`

Method invocation `lookupVar` may produce `NullPointerException`

Casting `lit` to `AbstractIntegerLiteral` may produce `ClassCastException`

Method invocation `getContainerType` may produce `NullPointerException`

Method invocation `multiply` may produce `NullPointerException`

Method invocation `negate` may produce `NullPointerException`

Argument `numbers` might be null

Method invocation `iterator` may produce `NullPointerException`

Method invocation `iterator` may produce `NullPointerException`

Variable is already assigned to this value

Result of `toReturn.size()` is always '0'

Result of `toReturn.size()` is always '0'

Method invocation `longValue` may produce `NullPointerException`

Method invocation `and` may produce `NullPointerException`

Method invocation `not` may produce `NullPointerException`

Method invocation `longValue` may produce `NullPointerException`

Method invocation `concat` may produce `NullPointerException`

Method invocation `concat` may produce `NullPointerException`

Variable is already assigned to this value

Variable is already assigned to this value

Variable is already assigned to this value

Variable is already assigned to this value

Variable is already assigned to this value

Variable is already assigned to this value

Condition `b && term.occurs(a)` is always `false`

Condition `b` is always `false`

Condition `pats == null` is always `true` when reached

Condition `pats == null` is always `true` when reached

Variable is already assigned to this value

Condition `content != null` is always `true`

Argument `heap` might be null

Argument `heap` might be null

Argument `SMTHandlerServices.class.getResourceAsStream("preamble.smt2")` might be null

Argument `stream` might be null

Argument `ModularSMTLib2Translator.class.getResourceAsStream(s)` might be null

Condition `t2 == PrimitiveType.JAVA_LONG` is always `false` when reached

Condition `t2 == PrimitiveType.JAVA_FLOAT` is always `false` when reached

Condition `t2 == PrimitiveType.JAVA_DOUBLE` is always `false` when reached

Argument `makeAdmissibleName(fs.getName())` might be null

Condition `tdc instanceof recoder.java.CompilationUnit` is redundant and can be replaced with a null check

Argument `makeAdmissibleName(recoderVarSpec.getName())` might be null

Method invocation `equals` may produce `NullPointerException`

Condition `getCause() instanceof de.uka.ilkd.key.parser.proofjava.ParseException` is redundant and can be replaced with a null check

Casting `result` to `KeYJavaType` may produce `ClassCastException`

Condition `rp instanceof recoder.java.reference.ReferenceSuffix` is always `true`

Method invocation `getJavaType` may produce `NullPointerException`

Condition `containerType != null` is always `true`

Condition `visibleToPackage` is always `false` when reached

Method invocation `equals` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Condition `instArray.last() instanceof ProgramElement` is redundant and can be replaced with a null check

Dereference of `changeList` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `isEmpty` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `size` may produce `NullPointerException`

Method invocation `toString` may produce `NullPointerException`

Method invocation `isEmpty` may produce `NullPointerException`

Method invocation `add` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `add` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `size` may produce `NullPointerException`

Method invocation `isEmpty` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `size` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `isEmpty` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `toString` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Method invocation `isEmpty` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `isEmpty` may produce `NullPointerException`

Method invocation `isEmpty` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `toString` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `add` may produce `NullPointerException`

Method invocation `size` may produce `NullPointerException`

Method invocation `getFirst` may produce `NullPointerException`

Method invocation `equals` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Method invocation `get` may produce `NullPointerException`

Condition `body instanceof StatementBlock` is always `false`

Condition `body != null` is always `true`

Condition `body != null` is always `true`

Condition `identifier instanceof IProgramVariable` is redundant and can be replaced with a null check

Method invocation `get` may produce `NullPointerException`

Method invocation `getSort` may produce `NullPointerException`

Method invocation `size` may produce `NullPointerException`

Method invocation `size` may produce `NullPointerException`

Method invocation `getName` may produce `NullPointerException`

Method invocation `getName` may produce `NullPointerException`

Condition `r != null` is always `true`

Condition `r != null` is always `true`

Casting `q` to `Ccatch` will produce `ClassCastException` for any non-null value

Method invocation `equals` may produce `NullPointerException`

Unboxing of `children.get(Boolean.class)` may produce `NullPointerException`

Condition `nameclash` is always `false`

Argument `term` might be null

Argument `selfTerm` might be null

Dereference of `furtherLocs` may produce `NullPointerException`

Dereference of `furtherLocs` may produce `NullPointerException`

Argument `anonAssumption` might be null