Least opaque predicates

[stefan-aws]

Dafny version

3.11.0.50201

Code to produce this issue

least predicate {:opaque} P(x: int) {
  x == 0
}

lemma L(n: nat) 
{
  reveal P();
  assert P(0);
}

Command to run and resulting output

(1,26): Error: wrong number of arguments to function: _module.__default.P (1 instead of 2)
...
4 type checking errors detected in /var/folders/0j/f_c89qx51zxd2f1wpyqqtclm0000gr/T/fail_example_1__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/var/folders/0j/f_c89qx51zxd2f1wpyqqtclm0000gr/T/fail_example_1__module.bpl(3235,6): Error: wrong number of arguments to function: _module.__default.P (1 instead of 2)

What happened?

Without {:opaque}, the code verifies and compiles:

least predicate P(x: int) {
  x == 0
}

lemma L(n: nat) 
{
  assert P(0);
}

It seems as if least predicates with opaque require a recursive call. For example, this snippet goes through:

// even naturals
least predicate {:opaque} P(x: int) {
  (x == 0) || (x > 0 && P(x-2))
} 
lemma L() {
  reveal P();
  assert P(0);
}

What type of operating system are you experiencing the problem on?

Mac

[MikaelMayer]

Related to
#3506