VerCors throws an error when Specifying a resource as trigger

[sakehl]

resource test(int i) = i > 0;

void main(){
   loop_invariant i >= 0 && i <= 10;
   loop_invariant (\forall* int j; 0 <= j && j <= i; {:test(j):});
  for(int i = 0; i < 10; i++){
    fold test(i);
  }

}

This program throws the error:

Caused by: java.lang.RuntimeException: Unexpected expression acc(test(j), write) cannot be symbolically evaluated
    at scala.sys.package$.error(package.scala:27)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:1061)

When not specifying the trigger, this does not happen.

Additional remark: when you 'forget' to write fold and write:

resource test(int i) = i > 0;

void main(){
   loop_invariant i >= 0 && i <= 10;
   loop_invariant (\forall* int j; 0 <= j && j <= i; {:test(j):});
  for(int i = 0; i < 10; i++){
    test(i);
  }

}

we get:

.
viper.api.transform.ColToSilver$NotSupported: ======================================
20     int flatten1;
   21     ref excbeforeloop;
         [--------
   22     resource evaluationdummy;
          --------]
   23     exc := null
   24     label LOOP;
--------------------------------------
This kind of node (TResource) is not supported by silver directly. Is there a rewrite missing?

[pieter-bos]

Re: second error: Eval should coerce its value to TAnyValue, that should resolve it. The correct solution is actually that you're allowed to write it, since VerCors supports resource values now.