Implement scaling of instance predicates

src/main/vct/main/stages/Transformation.scala

@@ -239,6 +239,7 @@ case class SilverTransformation
     ResolveExpressionSideEffects,
     EncodeTryThrowSignals,
 
+    ResolveScale,
     // No more classes
     ClassToRef,
 
@@ -274,7 +275,6 @@ case class SilverTransformation
 
     // Silver compat (basically no new nodes)
     FinalizeArguments,
-    ResolveScale,
     ExplicitADTTypeArgs,
     ForLoopToWhileLoop,
     BranchToIfElse,

src/rewrite/vct/rewrite/ResolveScale.scala

@@ -60,6 +60,7 @@ case class ResolveScale[Pre <: Generation]() extends Rewriter[Pre] {
       case Value(loc) =>
         (amount > NoPerm()) ==> Value(dispatch(loc))
       case apply: PredicateApply[Pre] => apply.rewrite(perm = amount * dispatch(apply.perm))
+      case apply: InstancePredicateApply[Pre] => apply.rewrite(perm = amount * dispatch(apply.perm))
 
       case Star(left, right) => scale(left, amount) &* scale(right, amount)
       case Implies(cond, cons) => Implies(dispatch(cond), scale(cons, amount))

test/main/vct/test/integration/examples/TechnicalSpec.scala

@@ -443,5 +443,17 @@ vercors should verify using silicon in "example using string primitive" pvl
     @*/
     void test();
   """
+
+  vercors should verify using silicon in "unfold scaled instance predicate" pvl
+    """
+    class C {
+      resource P (int x) = true;
+
+      requires [1\2]P(0);
+      void m (int x) {
+        unfold [1\3]P(0);
+      }
+    }
+    """
 }