Skip to content

stepf does not skip splits with succesfull nodes #3073

Open
@virgil-serbanuta

Description

@virgil-serbanuta

To reproduce:

Versions:

$ kompile --version test.k --backend haskell && kprove proof.k --haskell-backend-command 'kore-repl --version'
K version:    v5.3.60-0-gbf6c9cb9d0
Build date:   Wed May 25 19:59:21 EEST 2022
Kore version 0.60.0.0
Git:
  revision:     9767a2a2598f2f9e3ad969ac3ba0d81d1a26a9aa
  branch:       HEAD
  last commit:  Fri May 20 09:13:31 2022 -0600
Welcome to the Kore Repl! Use 'help' to get started.
...

test.k

module TEST
  imports BOOL
  imports INT

  syntax KItem ::= split(KItem) | "a" | "b"

  rule split(_:Int) => a
  rule split(K:KItem) => b ensures notBool isInt(K)

  rule a => .K
endmodule

proof.k

module PROOF
  imports TEST

  claim split(A:KItem) => .K requires isInt(A)
endmodule

Command line:

kompile --version test.k --backend haskell && kprove proof.k --haskell-backend-command 'kore-repl --version'

Repl:

step
stepf

Expected result: the current node should be '1'.
Actual result: the current node is '0'.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions