Crash while typechecking

[abakst]

I get a crash when executing the SAW script

env <- heapster_init_env // ...
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
heapster_typecheck_fun env "foo"
  "(). arg0:array(W,0,<5,*8,fieldsh(int64<>)) -o arg0:array(W,0,<5,*8,fieldsh(int64<>)),ret:int64<>";

with foo defined:

uint64_t foo(uint64_t *y) {
  uint64_t *p = &y[0];
  for (uint64_t i = 0; i < 5; ++i) {
    p = &y[i];
  }
  return 0;
}

the C is compiled via clang -fno-inline -emit-llvm -g -c

The crash is:

[23:12:00.224] proveVarImpl: incorrect permission on top of the stack
expected: eq(top_ptr) actual: eq(top_ptr &+ 0)
CallStack (from HasCallStack):
  error, called at src/Verifier/SAW/Heapster/Implication.hs:7710:67 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.Implication