Spawn exhales permissions of called procedure, but never inhales them

[jsalzbergedu]

Expected Behavior

When running raven on the following file:

field myThreadData: Int;

proc readData(x: Ref)
  requires readPerms(x)
  ensures readPerms(x) {
}

pred readPerms(x: Ref) {
  (exists q: Real :: own(x, myThreadData, 10, q))
}

proc useMyThreadDataConcurrently(theData: Ref) ensures readPerms(theData) {
  theData := new (myThreadData: 10);
  fold readPerms(theData)[q := 0.5];
  fold readPerms(theData)[q := 0.5];
  spawn readData(theData);
  spawn readData(theData);
}

I expect to see "Verification Successful."

Actual Behavior

I get the error:

[Error] File "./concurrently.rav", line 12, columns 55-73:
12 | proc useMyThreadDataConcurrently(theData: Ref) ensures readPerms(theData) {
                                                            ^^^^^^^^^^^^^^^^^^
Related Location: This is the postcondition that may not hold.

and in the log.smt2 I see:

...
; Inhale stmt for Call: spawn readData(theData)
; inhale: true ==> true 
...
; Exhale stmt for Call: spawn readData(theData)
; exhale: true ==> readPerms(theData) 
...

Specifications

This is run on version 198c96c

Thanks!

[jsalzbergedu]

I see, one would have to set the pre-and-post conditions as an invariant. then the code compiles