1
Vote

Boogie error when scaling read permissions

description

The Chalice program
class Test {
  predicate P { rd(mu) }
  
  method test2()
    requires P
    requires unfolding rd(P) in true
  {}
}
results in the Boogie error
stdin.bpl(454,52): Error: invalid argument types (int and real) to binary operator *
Chalice (hg id -nibt): 61af32ca9b60+ 483+ default tip
Boogie: 2.2.30705.1126

comments