Error transformer not working with Silicon

I was working on a plugin for a school project (which I've now submitted). I tried using an error transformer with VSCode, but when I tested it the errors appeared transformed when using Carbon but not when using Silicon. If I switched from Carbon to Silicon then Silicon would work (maybe to do with caching). The code for the plugin is part of a fork of Silver https://github.com/dewert99/silver/tree/pred-inline An example viper program that shows this issue when using the plugin is:

field x: Int

inline predicate test(r: Ref) {acc(r.x) && r.x > 0}

method foo(r: Ref)
{
  assert unfolding test(r) in r.x > 0
}

which my plugin expands to

domain __SECOND__[T] {

  function __second__(b: Bool, t: T): T

  axiom {
    (forall b: Bool, t: T :: { (__second__(b, t): T) } (__second__(b, t): T) == t)
  }
}

field x: Int

function __unfolding_test__(r: Ref, __perm__: Perm): Bool
  requires __perm__ >= none && (__perm__ > none ==> acc(r.x, write * __perm__) && r.x > 0)
{
  true
}

method foo(r: Ref)
{
  assert (__second__(__unfolding_test__(r, write), r.x > 0): Bool)
}

On Silicon this gives: Precondition of function __unfolding_test__ might not hold. There might be insufficient permission to access r.x (test.vpr@7.19--8.1)

On Carbon this gives: Assert might fail. There might be insufficient permission to access test(r) (test.vpr@7.9--7.10) Assert might fail. There might be insufficient permission to access r.x (test.vpr@7.9--7.10)

Switching back to Silicon gives: Assert might fail. There might be insufficient permission to access test(r) (test.vpr@7.9--7.10)

viperproject / silver

Error transformer not working with Silicon #550