User-defined sorts cannot be referenced in quantified expressions

KeYProject / key

KeY Theorem Prover for Deductive Java Verification

https://key-project.org

Other

41 stars 24 forks source link

User-defined sorts cannot be referenced in quantified expressions #3404

Open mattulbrich opened 6 months ago

mattulbrich commented 6 months ago

## Description User-defined/Built-in KeY sorts are supposed to be accessible from within JML using a `\dl_` escape. However, this does not work within quantified expressions. ### Steps to reproduce always ``` final class C { //@ invariant (\forall \dl_Seq c; c == c); } ``` does not load in KeY. -- * Commit: 7fe4e7dba53801c38716889cec9241488ce31680

mattulbrich commented 6 months ago

And they cannot be used in cast expressions either. (\dl_Seq)x reportedly tends to fail, too.