Skip to content

nondet shadows variable initialization #1820

Description

@erickpintor

Model:

module foo {
  var bar: int

   action init =
     nondet bar = Nat.oneOf() // <- same name as var
     bar' = bar

  action step =
    bar' = bar + 1
}

Run:

$ quint run foo.qnt
/Users/erickpintor/Downloads/foo.qnt:9:12 - error: [QNT502] Variable bar not set
9:     bar' = bar + 1
              ^^^

error: Runtime error

Fix: allow shadowing but assign the shadowed value to the primed var.

Note: failed both in typescript and rust backends.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions