Mattias Ulbrich

If `-init-pred` is used as command-line parameter, the program produces illegal SMT2 code which has nested `assert` commands. ```` (assert (assert (forall ((n$1_0 Int) (n$2_0 Int)) (=> (IN_INV n$1_0 n$2_0)...

Assertion failure in llreve-dynamic

2

Hej, I tried to use the llreve-dyamic tool on the following example: ``` extern int __mark(int); void send(int *to, int *from, int count) { do { /* count > 0...

Control-C may leave a defunct process

2

## Description When starting KeY from the command line, pressing ctrl-c prior to the main window's appearance leaves KeY in a defunct state that can only be killed from outside....

## Description KeY used to have support for a model method modifier `no_state` indicating that a method must not at all read from the heap. Now, using `no_state` makes KeY...

MixFix Parsing - An idea

1

This PR is meant as a wip - tryout - branch for mixfix parsing in KeY ## Related Issue We want to define syntax for symbols in .key files. This...

User-defined sorts cannot be referenced in quantified expressions

1

## 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...

Assertions in ifs raise exceptions

2

## Description Using assertions as ~last~ statement inside an **(otherwise empty)** if-then-block raises a class cast exception ## Reproducible always. ### Steps to reproduce Try to load: ```java class A...

Revert "Fix CurrentGoalView highlights not being removed"

4

## Related Issue This pull request addresses #3378. ## Intended Change This reverts commit 4759370f719ed506746e7a2a13832eac48cfc6c1. As discussed during a developers meeting, the highlighting is quite important during drag'n'drop. It reenables...

## Description It used to be that the formula which becomes the target of a drag-and-drop activity was highlighted in green. This is no longer the case since commit 4759370f719ed506746e7a2a13832eac48cfc6c1...

Logical Infrastructure for final values independent from the heap

1

**This is a copy of [Merge Request !318 at gitlab](https://git.key-project.org/key/key/-/merge_requests/318). See also there for an extensive discussion on the subject.** ### Constructors This mechanism *must not* be used when verifying...