Uncaught exception during generation of PO for accessible \strictly_nothing on model field

[WolframPfeifer]

Description

When you try to start a proof of a dependency contract of a model field that contains \strictly_nothing, an exception is thrown during generation of the proof obligation.

Reproducible

always

Steps to reproduce

1. Load this example class:

   public final class Test {
       //@ model int mfield;
       //@ represents mfield = 42;
       //@ accessible mfield: \strictly_nothing;
   }
   

2. In the proof management dialog, try to start the proof of the accessible clause.

In the GUI, nothing happens. In the CLI, you can see a TermCreationException.

Expected behavior would be that an error is shown in the IssueDialog with position information (or should it even be allowed, although not necessary, since model fields can not create new objects?).

Additional Information

• Stack trace:

Exception in thread "AWT-EventQueue-0" de.uka.ilkd.key.logic.TermCreationException: Building a term failed. Normally there is an arity mismatch or one of the subterms' sorts is not compatible (e.g. like the '2' in "true & 2")
The top level operator was setMinus(Sort: LocSet); its expected arg sorts were:
1.) sort: LocSet, sort hash: 2036281275
2.) sort: LocSet, sort hash: 2036281275

The subterms were:
1.) allLocs(sort: LocSet, sort hash: 2036281275)
2.) false(sort: Formula, sort hash: 453996890)

	at de.uka.ilkd.key.logic.op.AbstractSortedOperator.additionalValidTopLevel(AbstractSortedOperator.java:95)
	at de.uka.ilkd.key.logic.op.AbstractOperator.validTopLevelException(AbstractOperator.java:99)
	at de.uka.ilkd.key.logic.op.AbstractSortedOperator.validTopLevelException(AbstractSortedOperator.java:16)
	at de.uka.ilkd.key.logic.TermImpl.checked(TermImpl.java:144)
	at de.uka.ilkd.key.logic.TermFactory.doCreateTerm(TermFactory.java:129)
	at de.uka.ilkd.key.logic.TermFactory.createTerm(TermFactory.java:64)
	at de.uka.ilkd.key.logic.TermFactory.createTerm(TermFactory.java:76)
	at de.uka.ilkd.key.logic.TermFactory.createTerm(TermFactory.java:81)
	at de.uka.ilkd.key.logic.TermBuilder.func(TermBuilder.java:403)
	at de.uka.ilkd.key.logic.TermBuilder.setMinus(TermBuilder.java:1369)
	at de.uka.ilkd.key.proof.init.DependencyContractPO.readProblem(DependencyContractPO.java:200)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.startProver(ProblemInitializer.java:577)
	at de.uka.ilkd.key.gui.ProofManagementDialog.findOrStartProof(ProofManagementDialog.java:470)
	at de.uka.ilkd.key.gui.ProofManagementDialog.lambda$new$5(ProofManagementDialog.java:213)
	at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1972)
	...

• Commit: f798501f0dc35fb70b19461bbf32dfbf8f7e869b (current main)