From 01defeabd22cd3db5208b0900ff2c9d819c2ccbf Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Tue, 11 May 2021 16:46:52 +0200
Subject: [PATCH 1/6] Get code from branch predicate-refactor to avoid merge
 commit

---
 examples/predicates/ScaleInlinePredicate.pvl  |  37 ++++
 .../rewrite/InlinePredicatesFunctions.java    | 175 ++++++++++++++++++
 2 files changed, 212 insertions(+)
 create mode 100644 examples/predicates/ScaleInlinePredicate.pvl
 create mode 100644 src/main/java/vct/col/rewrite/InlinePredicatesFunctions.java

diff --git a/examples/predicates/ScaleInlinePredicate.pvl b/examples/predicates/ScaleInlinePredicate.pvl
new file mode 100644
index 0000000000..d3f066b5b5
--- /dev/null
+++ b/examples/predicates/ScaleInlinePredicate.pvl
@@ -0,0 +1,37 @@
+//:: cases ScaleInlinePredicate
+//:: tools silicon
+//:: verdict Pass
+
+class C {
+    int x;
+    int y;
+    inline resource r() = Perm(x, write);
+
+    inline resource s() = r() ** Perm(y, 1\2) ** x == y;
+
+    requires [1\2]r();
+    void m() {
+        unfold [1\2]r();
+        assert Perm(x, 1\2);
+    }
+
+    requires [1\4]r();
+    void m2() {
+        unfold [1\2][1\2]r();
+        assert Perm(x, 1\4);
+    }
+
+    requires s();
+    void m3() {
+        fold [1\2]s();
+        assert x == y;
+        assert Perm(y, 1\2) ** Perm(x, write);
+    }
+
+    requires [1\8]s();
+    void m4() {
+        fold [1\4][1\4]s();
+        assert x == y;
+        assert Perm(y, 1\16) ** Perm(x, 1\8);
+    }
+}
diff --git a/src/main/java/vct/col/rewrite/InlinePredicatesFunctions.java b/src/main/java/vct/col/rewrite/InlinePredicatesFunctions.java
new file mode 100644
index 0000000000..9a7b2e4081
--- /dev/null
+++ b/src/main/java/vct/col/rewrite/InlinePredicatesFunctions.java
@@ -0,0 +1,175 @@
+package vct.col.rewrite;
+
+import vct.col.ast.expr.NameExpression;
+import vct.col.ast.stmt.decl.ASTFlags;
+import vct.col.ast.generic.ASTNode;
+import vct.col.ast.stmt.decl.ASTSpecial;
+import vct.col.ast.stmt.decl.Method;
+import vct.col.ast.expr.MethodInvokation;
+import vct.col.ast.expr.OperatorExpression;
+import vct.col.ast.stmt.decl.ProgramUnit;
+import vct.col.ast.expr.StandardOperator;
+import vct.col.ast.type.ASTReserved;
+import vct.col.ast.util.AbstractRewriter;
+
+import java.util.HashMap;
+import java.util.Stack;
+
+// Also: doublecheck if output predicate have _predicate instead of _constructor
+
+public class InlinePredicatesFunctions extends AbstractRewriter {
+
+  int count = 0;
+  Stack<String> inlinedScalars = new Stack<>();
+ 
+  public InlinePredicatesFunctions(ProgramUnit source) {
+    super(source);
+  }
+
+  public ASTNode inlineCall(MethodInvokation e, Method def) {
+    int N=def.getArity();
+    HashMap<NameExpression,ASTNode> map=new HashMap<NameExpression, ASTNode>();
+    Substitution sigma=new Substitution(source(),map);
+    map.put(create.reserved_name(ASTReserved.This), rewrite(e.object()));
+    for(int i=0;i<N;i++){
+      map.put(create.unresolved_name(def.getArgument(i)),rewrite(e.getArg(i)));
+    }
+    ASTNode body=rewrite(def.getBody());
+    InlineMarking marker=new InlineMarking(source(),e.getOrigin());
+    body.accept(marker);
+    return sigma.rewrite(body);
+  }
+
+  @Override
+  public void visit(MethodInvokation e){
+    if (inline(e)){
+      result = inlineCall(e, e.getDefinition());
+    } else if (!inlinedScalars.empty() && e.getDefinition().getKind().equals(Method.Kind.Predicate)) {
+      // Because the previous if branch was false, we know this is a predicate that is not inline
+      // Hence, we have to add a scale that scales the predicate according to any earlier encountered scales
+      super.visit(e);
+      result = create.expression(StandardOperator.Scale,
+              getCombinedScalar(null),
+              result
+              );
+    } else {
+      super.visit(e);
+    }
+  }
+
+  protected boolean inline(ASTNode node) {
+    if (node instanceof Method) {
+      Method def = (Method) node;
+      if (def.isValidFlag(ASTFlags.INLINE)){
+        return (def.kind==Method.Kind.Predicate || def.kind==Method.Kind.Pure) && def.getFlag(ASTFlags.INLINE);
+      } else {
+        return false;
+      }
+    } else if (node instanceof MethodInvokation) {
+      MethodInvokation invokation = (MethodInvokation) node;
+      return inline(invokation.getDefinition());
+    } else if (node instanceof OperatorExpression) {
+      OperatorExpression operatorExpression = (OperatorExpression) node;
+      if (operatorExpression.operator() == StandardOperator.Scale) {
+        return inline(operatorExpression.arg(1));
+      }
+    }
+
+    return false;
+  }
+
+  @Override
+  public void visit(Method m){
+    if (inline(m)){
+      result=null;
+    } else {
+      super.visit(m);
+    }
+  }
+
+  /**
+   * Returns all the aggregated scalars so far in one multiplication.
+   *
+   * Given a startNode, it will yield the following AST:
+   *
+   * (((startNode * scalar1) * scalar2) * ...
+   *
+   * If no startNode is given, only the scalars appear in the tree.
+   *
+   * The reason startNode is a possible argument is because of a bug in Viper where if startNode
+   * is not at the bottom of a multiplication tree, some type error is triggered in Viper. Ideally,
+   * this method would have no arguments, and would just return the multiplication tree of the scalars.
+   *
+   * @param startNode Node to start the multiplication with. If not available, can be null.
+   * @return AST corresponding to: (((startNode * scalar1) * scalar2) * ...
+   */
+  private ASTNode getCombinedScalar(ASTNode startNode) {
+    if (inlinedScalars.empty()) {
+      Abort("Cannot combine scalars when stack is empty");
+    }
+
+    ASTNode result;
+    int startIndex;
+
+    if (startNode == null) {
+      result = create.local_name(inlinedScalars.get(0));
+      startIndex = 1;
+    } else {
+      result = startNode;
+      startIndex = 0;
+    }
+
+    for (int i = startIndex; i < inlinedScalars.size(); i++) {
+      result = create.expression(
+              StandardOperator.Mult,
+              result,
+              create.local_name(inlinedScalars.get(i)));
+    }
+
+    return result;
+  }
+
+  @Override
+  public void visit(OperatorExpression e){
+    switch(e.operator()){
+      case Scale:
+        if (inline(e)) {
+          String scaleAmountName = "inlineScalar" + count++;
+
+          inlinedScalars.push(scaleAmountName);
+          super.visit(e);
+          OperatorExpression scaleExpr = (OperatorExpression) result;
+          inlinedScalars.pop();
+
+          result = create.let_expr(
+                  create.field_decl(scaleAmountName, rewrite(e.arg(0).getType()), scaleExpr.arg(0)),
+                  scaleExpr.arg(1)
+          );
+        } else {
+          super.visit(e);
+        }
+        break;
+      case Perm:
+        super.visit(e);
+        OperatorExpression newPerm = (OperatorExpression) result;
+        if (!inlinedScalars.empty()) {
+          ASTNode permissionAmount = getCombinedScalar(e.arg(1));
+          result = create.expression(StandardOperator.Perm, newPerm.arg(0), permissionAmount);
+        }
+        break;
+      default:
+        super.visit(e);
+        break;
+    }
+  }
+
+  @Override
+  public void visit(ASTSpecial e) {
+    if (e.kind == ASTSpecial.Kind.Fold || e.kind == ASTSpecial.Kind.Unfold) {
+      Warning("Folding/unfolding an inline predicate is allowed but not encouraged. See https://github.com/utwente-fmt/vercors/wiki/Resources-and-Predicates#inline-predicates for more info.");
+      create.special(ASTSpecial.Kind.Assert, rewrite(e.getArg(0)));
+    } else {
+      super.visit(e);
+    }
+  }
+}

From 59dd60febbc7edf4cf0a65316395cccb4ff40be4 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Tue, 11 May 2021 17:00:56 +0200
Subject: [PATCH 2/6] Turn on the new predicate inline pass.

---
 ...java => InlinePredicatesAndFunctions.java} |   6 +-
 .../col/rewrite/InlinePredicatesRewriter.java | 110 ------------------
 src/main/java/vct/main/Passes.scala           |   2 +-
 3 files changed, 3 insertions(+), 115 deletions(-)
 rename src/main/java/vct/col/rewrite/{InlinePredicatesFunctions.java => InlinePredicatesAndFunctions.java} (96%)
 delete mode 100644 src/main/java/vct/col/rewrite/InlinePredicatesRewriter.java

diff --git a/src/main/java/vct/col/rewrite/InlinePredicatesFunctions.java b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
similarity index 96%
rename from src/main/java/vct/col/rewrite/InlinePredicatesFunctions.java
rename to src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
index 9a7b2e4081..0b1311c824 100644
--- a/src/main/java/vct/col/rewrite/InlinePredicatesFunctions.java
+++ b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
@@ -15,14 +15,12 @@
 import java.util.HashMap;
 import java.util.Stack;
 
-// Also: doublecheck if output predicate have _predicate instead of _constructor
-
-public class InlinePredicatesFunctions extends AbstractRewriter {
+public class InlinePredicatesAndFunctions extends AbstractRewriter {
 
   int count = 0;
   Stack<String> inlinedScalars = new Stack<>();
  
-  public InlinePredicatesFunctions(ProgramUnit source) {
+  public InlinePredicatesAndFunctions(ProgramUnit source) {
     super(source);
   }
 
diff --git a/src/main/java/vct/col/rewrite/InlinePredicatesRewriter.java b/src/main/java/vct/col/rewrite/InlinePredicatesRewriter.java
deleted file mode 100644
index 8745fe2c94..0000000000
--- a/src/main/java/vct/col/rewrite/InlinePredicatesRewriter.java
+++ /dev/null
@@ -1,110 +0,0 @@
-package vct.col.rewrite;
-
-import vct.col.ast.expr.NameExpression;
-import vct.col.ast.stmt.decl.ASTFlags;
-import vct.col.ast.generic.ASTNode;
-import vct.col.ast.stmt.decl.ASTSpecial;
-import vct.col.ast.stmt.decl.Method;
-import vct.col.ast.expr.MethodInvokation;
-import vct.col.ast.expr.OperatorExpression;
-import vct.col.ast.stmt.decl.ProgramUnit;
-import vct.col.ast.expr.StandardOperator;
-import vct.col.ast.type.ASTReserved;
-import vct.col.ast.util.AbstractRewriter;
-
-import java.util.HashMap;
-
-public class InlinePredicatesRewriter extends AbstractRewriter {
- 
-  public InlinePredicatesRewriter(ProgramUnit source) {
-    super(source);
-  }
-
-  public ASTNode inline_call(MethodInvokation e, Method def) {
-    int N=def.getArity();
-    HashMap<NameExpression,ASTNode> map=new HashMap<NameExpression, ASTNode>();
-    Substitution sigma=new Substitution(source(),map);
-    map.put(create.reserved_name(ASTReserved.This), rewrite(e.object()));
-    for(int i=0;i<N;i++){
-      map.put(create.unresolved_name(def.getArgument(i)),rewrite(e.getArg(i)));
-    }
-    ASTNode body=rewrite(def.getBody());
-    InlineMarking marker=new InlineMarking(source(),e.getOrigin());
-    body.accept(marker);
-    return sigma.rewrite(body);
-  }
-
-  @Override
-  public void visit(MethodInvokation e){
-    Method def=e.getDefinition();
-    boolean inline;
-    if (def==null){
-      inline=false;
-    } else {
-      inline = inline(def);
-    }
-    if (inline){
-      result=inline_call(e, def);
-    } else {
-      super.visit(e);
-    }
-  }
-
-  protected boolean inline(Method def) {
-    boolean inline;
-    if (def.isValidFlag(ASTFlags.INLINE)){
-      inline=(def.kind==Method.Kind.Predicate || def.kind==Method.Kind.Pure) && def.getFlag(ASTFlags.INLINE);
-    } else {
-      inline=false;
-    }
-    return inline;
-  }
-
-  @Override
-  public void visit(Method m){
-    if (inline(m)){
-      result=null;
-    } else {
-      super.visit(m);
-    }
-  }
-  
-  @Override
-  public void visit(OperatorExpression e){
-    switch(e.operator()){
-      case Unfolding:
-      {
-        ASTNode arg1=rewrite(e.arg(0));
-        ASTNode arg2=rewrite(e.arg(1));
-        if (arg1 instanceof MethodInvokation || arg1.isa(StandardOperator.Scale)){
-          result=create.expression(StandardOperator.Unfolding,arg1,arg2);
-        } else {
-          result=arg2;
-        }
-        break;
-      }
-      default:
-        super.visit(e);
-        break;
-    }
-  }
-  @Override
-  public void visit(ASTSpecial e){
-    switch(e.kind){
-      case Unfold:
-      case Fold:
-      { 
-        ASTNode arg=rewrite(e.getArg(0));
-        if (arg instanceof MethodInvokation || arg.isa(StandardOperator.Scale)){
-          result=create.special(e.kind,arg);
-        } else {
-          result=null; // returning null for a statement means already inserted or omit.
-        }
-        break;
-      }
-      default:
-        super.visit(e);
-        break;
-    }
-  }
-}
diff --git a/src/main/java/vct/main/Passes.scala b/src/main/java/vct/main/Passes.scala
index b6b0d922a4..6df9094b4d 100644
--- a/src/main/java/vct/main/Passes.scala
+++ b/src/main/java/vct/main/Passes.scala
@@ -475,7 +475,7 @@ object Passes {
     ),
     SimplePass("inline",
       "inlineInlineMethods",
-      new InlinePredicatesRewriter(_).rewriteAll,
+      new InlinePredicatesAndFunctions(_).rewriteAll,
       permits=Feature.DEFAULT_PERMIT - features.Lemma - features.MethodAnnotations + features.TopLevelImplementedMethod + features.TopLevelMethod,
       removes=Set(features.InlinePredicate)),
     ErrorMapPass(

From 23c9e06b14b38effd78b91c43d530c8049366941 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Tue, 11 May 2021 17:27:08 +0200
Subject: [PATCH 3/6] Disallow recursive inline predicates.

---
 .../MutuallyRecursiveInlinePredicates.pvl     | 12 ++++++++++++
 .../predicates/RecursiveInlinePredicate.pvl   | 11 +++++++++++
 .../rewrite/InlinePredicatesAndFunctions.java | 19 +++++++++++++++++--
 3 files changed, 40 insertions(+), 2 deletions(-)
 create mode 100644 examples/predicates/MutuallyRecursiveInlinePredicates.pvl
 create mode 100644 examples/predicates/RecursiveInlinePredicate.pvl

diff --git a/examples/predicates/MutuallyRecursiveInlinePredicates.pvl b/examples/predicates/MutuallyRecursiveInlinePredicates.pvl
new file mode 100644
index 0000000000..87ef014423
--- /dev/null
+++ b/examples/predicates/MutuallyRecursiveInlinePredicates.pvl
@@ -0,0 +1,12 @@
+//:: cases MutuallyRecursiveInlinePredicates
+//:: tools silicon
+//:: verdict Error
+
+class C {
+    inline resource p() = q() ** true;
+    inline resource q() = true ** p();
+
+    void p() {
+        assert p();
+    }
+}
diff --git a/examples/predicates/RecursiveInlinePredicate.pvl b/examples/predicates/RecursiveInlinePredicate.pvl
new file mode 100644
index 0000000000..81f253df9a
--- /dev/null
+++ b/examples/predicates/RecursiveInlinePredicate.pvl
@@ -0,0 +1,11 @@
+//:: cases RecursiveInlinePredicate
+//:: tools silicon
+//:: verdict Error
+
+class C {
+    inline resource p() = true ** p();
+
+    void p() {
+        assert p();
+    }
+}
diff --git a/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
index 0b1311c824..455b4dabdc 100644
--- a/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
+++ b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
@@ -11,20 +11,32 @@
 import vct.col.ast.expr.StandardOperator;
 import vct.col.ast.type.ASTReserved;
 import vct.col.ast.util.AbstractRewriter;
+import vct.test.ThreadPool;
 
 import java.util.HashMap;
+import java.util.IdentityHashMap;
 import java.util.Stack;
 
+import static hre.lang.System.Output;
+
 public class InlinePredicatesAndFunctions extends AbstractRewriter {
 
   int count = 0;
   Stack<String> inlinedScalars = new Stack<>();
- 
+  IdentityHashMap<Method, Object> currentlyBeingInlined = new IdentityHashMap<>();
+
   public InlinePredicatesAndFunctions(ProgramUnit source) {
     super(source);
   }
 
   public ASTNode inlineCall(MethodInvokation e, Method def) {
+    if (currentlyBeingInlined.containsKey(def)) {
+      def.getOrigin().report("error", "Inline predicate or function cannot contain itself.");
+      hre.lang.System.Abort("Cyclical inline predicate or function detected");
+    } else {
+      currentlyBeingInlined.put(def, def);
+    }
+
     int N=def.getArity();
     HashMap<NameExpression,ASTNode> map=new HashMap<NameExpression, ASTNode>();
     Substitution sigma=new Substitution(source(),map);
@@ -35,7 +47,10 @@ public ASTNode inlineCall(MethodInvokation e, Method def) {
     ASTNode body=rewrite(def.getBody());
     InlineMarking marker=new InlineMarking(source(),e.getOrigin());
     body.accept(marker);
-    return sigma.rewrite(body);
+
+    ASTNode result = sigma.rewrite(body);
+    currentlyBeingInlined.remove(def);
+    return result;
   }
 
   @Override

From ceab803d7d848df13ed521a7bccf145088b9da94 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Wed, 12 May 2021 09:43:46 +0200
Subject: [PATCH 4/6] Add inline to feature system.

---
 examples/basic/InlineFunctions.pvl                  | 12 ++++++++++++
 src/main/java/vct/col/features/FeatureRainbow.scala | 12 ++++++++++--
 src/main/java/vct/main/Passes.scala                 |  2 +-
 3 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 examples/basic/InlineFunctions.pvl

diff --git a/examples/basic/InlineFunctions.pvl b/examples/basic/InlineFunctions.pvl
new file mode 100644
index 0000000000..56d9fbc10f
--- /dev/null
+++ b/examples/basic/InlineFunctions.pvl
@@ -0,0 +1,12 @@
+//:: cases InlineFunctions
+//:: tools silicon
+//:: verdict Pass
+
+class C {
+    ensures false;
+    inline int f() = 3 + 3;
+
+    void m() {
+        assert f() == 6;
+    }
+}
\ No newline at end of file
diff --git a/src/main/java/vct/col/features/FeatureRainbow.scala b/src/main/java/vct/col/features/FeatureRainbow.scala
index 3528b45a2b..c1eac6b957 100644
--- a/src/main/java/vct/col/features/FeatureRainbow.scala
+++ b/src/main/java/vct/col/features/FeatureRainbow.scala
@@ -171,8 +171,13 @@ class RainbowVisitor(source: ProgramUnit) extends RecursiveVisitor(source, true)
     }
 
     if(isPure(m)) {
-      if(isInline(m))
-        addFeature(InlinePredicate, m)
+      if(isInline(m)) {
+        if (m.getReturnType.isPrimitive(PrimitiveSort.Resource)) {
+          addFeature(InlinePredicate, m)
+        } else if (!m.getReturnType.isPrimitive(PrimitiveSort.Process)) {
+          addFeature(InlineFunction, m)
+        }
+      }
       if(m.getBody.isInstanceOf[BlockStatement])
         addFeature(PureImperativeMethods, m)
     }
@@ -618,6 +623,7 @@ object Feature {
     GivenYields,
     StaticFields,
     InlinePredicate,
+    InlineFunction,
     KernelClass,
     AddrOf,
     OpenMP,
@@ -746,6 +752,7 @@ object Feature {
     GivenYields,
     StaticFields,
     InlinePredicate,
+    InlineFunction,
     KernelClass,
     AddrOf,
     OpenMP,
@@ -846,6 +853,7 @@ case object ADTOperator extends ScannableFeature
 case object GivenYields extends ScannableFeature
 case object StaticFields extends ScannableFeature
 case object InlinePredicate extends ScannableFeature
+case object InlineFunction extends ScannableFeature
 case object KernelClass extends ScannableFeature
 case object AddrOf extends ScannableFeature
 case object OpenMP extends ScannableFeature
diff --git a/src/main/java/vct/main/Passes.scala b/src/main/java/vct/main/Passes.scala
index 6df9094b4d..5ae718d906 100644
--- a/src/main/java/vct/main/Passes.scala
+++ b/src/main/java/vct/main/Passes.scala
@@ -477,7 +477,7 @@ object Passes {
       "inlineInlineMethods",
       new InlinePredicatesAndFunctions(_).rewriteAll,
       permits=Feature.DEFAULT_PERMIT - features.Lemma - features.MethodAnnotations + features.TopLevelImplementedMethod + features.TopLevelMethod,
-      removes=Set(features.InlinePredicate)),
+      removes=Set(features.InlinePredicate, features.InlineFunction)),
     ErrorMapPass(
       "encodeMagicWands", "Encode magic wand proofs with abstract predicates",
       new WandEncoder(_, _).rewriteAll,

From 505530441b26af87664773b2b297bc24a09033ea Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Wed, 12 May 2021 10:18:56 +0200
Subject: [PATCH 5/6] Replace (un)fold of inline predicate with assert.

---
 .../java/vct/col/rewrite/InlinePredicatesAndFunctions.java    | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
index 455b4dabdc..e6036b4fe3 100644
--- a/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
+++ b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
@@ -178,9 +178,9 @@ public void visit(OperatorExpression e){
 
   @Override
   public void visit(ASTSpecial e) {
-    if (e.kind == ASTSpecial.Kind.Fold || e.kind == ASTSpecial.Kind.Unfold) {
+    if ((e.kind == ASTSpecial.Kind.Fold || e.kind == ASTSpecial.Kind.Unfold) && inline(e.args[0])) {
       Warning("Folding/unfolding an inline predicate is allowed but not encouraged. See https://github.com/utwente-fmt/vercors/wiki/Resources-and-Predicates#inline-predicates for more info.");
-      create.special(ASTSpecial.Kind.Assert, rewrite(e.getArg(0)));
+      result = create.special(ASTSpecial.Kind.Assert, rewrite(e.getArg(0)));
     } else {
       super.visit(e);
     }

From cb83d31ebd36233c69dfa3a38bde21aa2212b94e Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Wed, 12 May 2021 13:08:03 +0200
Subject: [PATCH 6/6] Update dead link.

---
 src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
index e6036b4fe3..440ac89e57 100644
--- a/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
+++ b/src/main/java/vct/col/rewrite/InlinePredicatesAndFunctions.java
@@ -179,7 +179,7 @@ public void visit(OperatorExpression e){
   @Override
   public void visit(ASTSpecial e) {
     if ((e.kind == ASTSpecial.Kind.Fold || e.kind == ASTSpecial.Kind.Unfold) && inline(e.args[0])) {
-      Warning("Folding/unfolding an inline predicate is allowed but not encouraged. See https://github.com/utwente-fmt/vercors/wiki/Resources-and-Predicates#inline-predicates for more info.");
+      Warning("Folding/unfolding an inline predicate is allowed but not encouraged. See https://github.com/utwente-fmt/vercors/wiki/Predicates#inline-predicates for more info.");
       result = create.special(ASTSpecial.Kind.Assert, rewrite(e.getArg(0)));
     } else {
       super.visit(e);