key icon indicating copy to clipboard operation
key copied to clipboard

Published 20 hours ago • verified publisher icon KeYProject

User-defined sorts cannot be referenced in quantified expressions

Open mattulbrich opened this issue 1 year ago • 1 comments

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 avatar Feb 12 '24 12:02 mattulbrich