Open marcoeilers opened 3 weeks ago
Thanks for the report. This is related to #1065 and #1133. As far as I know we basically don’t handle the cases where the termination checks fail. We should definitely do that at some point though since this message isn’t very helpful.
Crash Message
Version Information
2.2.0
HEAD
(changes=false)Arguments
/home/marco/git/vercors/examples/concepts/final/finalIntegerImpureError.java
File Inputs
/home/marco/git/vercors/examples/concepts/final/finalIntegerImpureError.java
```java public class MyClass { //@ decreases; private int f() { while (true) {} return 5; } } ```Full Log