diff --git a/src/main/scala/viper/silver/ast/Position.scala b/src/main/scala/viper/silver/ast/Position.scala
index 11146cf32..95ea4efcb 100644
--- a/src/main/scala/viper/silver/ast/Position.scala
+++ b/src/main/scala/viper/silver/ast/Position.scala
@@ -89,10 +89,10 @@ class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Opti
     file :: start :: end :: id :: Nil
 }
 
-object LineCol {
-  def apply(index: Int): (Int, Int) = {
+class LineCol(fp: FastParser) {
+  def getPos(index: Int): (Int, Int) = {
     // val Array(line, col) = ctx.input.prettyIndex(index).split(":").map(_.toInt)
-    val line_offset = FastParser._line_offset
+    val line_offset = fp._line_offset
     val result = java.util.Arrays.binarySearch(line_offset, index)
     if (result >= 0) {
       // Exact match
diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index 6cf495175..a179539ad 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/src/main/scala/viper/silver/ast/utility/Consistency.scala
@@ -8,7 +8,7 @@ package viper.silver.ast.utility
 
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Traverse
-import viper.silver.parser.FastParser
+import viper.silver.parser.{FastParser, FastParserCompanion}
 import viper.silver.verifier.ConsistencyError
 import viper.silver.{FastMessage, FastMessaging}
 
@@ -29,7 +29,7 @@ object Consistency {
     recordIfNot(suspect, !property, message)
 
   /** Names that are not allowed for use in programs. */
-  def reservedNames: Seq[String] = FastParser.keywords.toSeq
+  def reservedNames: Set[String] = FastParserCompanion.basicKeywords
 
   /** Returns true iff the string `name` is a valid identifier. */
   val identFirstLetter = "[a-zA-Z$_]"
diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 11324e86b..6b994cef9 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -53,19 +53,16 @@ object QuantifiedPermissions {
    *       e.g. someMethod.quantifiedFields.
    */
 
-  def quantifiedFields(root: Node, program: Program): collection.Set[Field] = {
+  def quantifiedFields(root: Member, program: Program): collection.Set[Field] = {
     val collected = mutable.LinkedHashSet[Field]()
     val visited = mutable.Set[Member]()
     val toVisit = mutable.Queue[Member]()
 
-    root match {
-      case m: Member => toVisit += m
-      case _ =>
-    }
+    toVisit += root
 
     toVisit ++= Nodes.referencedMembers(root, program)
 
-    quantifiedFields(toVisit, collected, visited, program)
+    quantifiedFields(toVisit, root, collected, visited, program)
 
     collected
   }
@@ -73,19 +70,16 @@ object QuantifiedPermissions {
   /* TODO: See comment above about caching
    * TODO: Unify with corresponding code for fields
    */
-  def quantifiedPredicates(root: Node, program: Program): collection.Set[Predicate] = {
+  def quantifiedPredicates(root: Member, program: Program): collection.Set[Predicate] = {
     val collected = mutable.LinkedHashSet[Predicate]()
     val visited = mutable.Set[Member]()
     val toVisit = mutable.Queue[Member]()
 
-    root match {
-      case m: Member => toVisit += m
-      case _ =>
-    }
+    toVisit += root
 
     toVisit ++= Nodes.referencedMembers(root, program)
 
-    quantifiedPredicates(toVisit, collected, visited, program)
+    quantifiedPredicates(toVisit, root, collected, visited, program)
 
     collected
   }
@@ -98,44 +92,69 @@ object QuantifiedPermissions {
   }
 
   private def quantifiedFields(toVisit: mutable.Queue[Member],
+                               root: Member,
                                collected: mutable.LinkedHashSet[Field],
                                visited: mutable.Set[Member],
                                program: Program): Unit = {
 
     while (toVisit.nonEmpty) {
-      val root = toVisit.dequeue()
-
-      root visit {
-        case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
-          collected += acc.loc.field
-        case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
+      val currentRoot = toVisit.dequeue()
+
+      val relevantNodes: Seq[Node] = currentRoot match {
+        case m@Method(_, _, _, pres, posts, _) if m != root =>
+          // use only specification of called methods
+          pres ++ posts
+        case f@Function(_, _, _, pres, posts, _) if f != root=>
+          // use only specification of called functions
+          pres ++ posts
+        case _ => Seq(currentRoot)
       }
 
-      visited += root
+      visited += currentRoot
 
-      utility.Nodes.referencedMembers(root, program) foreach (m =>
-        if (!visited.contains(m)) toVisit += m)
+      for (n <- relevantNodes){
+        n visit {
+          case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
+            collected += acc.loc.field
+          case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
+        }
+        utility.Nodes.referencedMembers(n, program) foreach (m =>
+          if (!visited.contains(m)) toVisit += m)
+      }
     }
   }
 
   private def quantifiedPredicates(toVisit: mutable.Queue[Member],
+                                   root: Member,
                                    collected: mutable.LinkedHashSet[Predicate],
                                    visited: mutable.Set[Member],
                                    program: Program): Unit = {
 
     while (toVisit.nonEmpty) {
-      val root = toVisit.dequeue()
-
-      root visit {
-        case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
-          collected += program.findPredicate(acc.loc.predicateName)
-        case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
+      val currentRoot = toVisit.dequeue()
+
+      val relevantNodes: Seq[Node] = currentRoot match {
+        case m@Method(_, _, _, pres, posts, _) if m != root =>
+          // use only specification of called methods
+          pres ++ posts
+        case f@Function(_, _, _, pres, posts, _) if f != root =>
+          // use only specification of called functions
+          pres ++ posts
+        case _ => Seq(currentRoot)
       }
 
-      visited += root
+      visited += currentRoot
 
-      utility.Nodes.referencedMembers(root, program) foreach (m =>
-        if (!visited.contains(m)) toVisit += m)
+      for (n <- relevantNodes){
+        n visit {
+          case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
+            collected += program.findPredicate(acc.loc.predicateName)
+          case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
+        }
+        utility.Nodes.referencedMembers(n, program) foreach (m =>
+          if (!visited.contains(m)) toVisit += m)
+
+      }
     }
   }
 
diff --git a/src/main/scala/viper/silver/cfg/CfgTest.scala b/src/main/scala/viper/silver/cfg/CfgTest.scala
index a07866420..f68961b83 100644
--- a/src/main/scala/viper/silver/cfg/CfgTest.scala
+++ b/src/main/scala/viper/silver/cfg/CfgTest.scala
@@ -36,7 +36,7 @@ object CfgTest {
   }
 
   private def parse[_: P](input: String, file: Path): Option[PProgram] = {
-    val result = FastParser.parse(input, file)
+    val result = new FastParser().parse(input, file)
     result match {
       case Parsed.Success(program@PProgram(_, _, _, _, _, _, _,_, errors), _) =>
         if (errors.isEmpty || errors.forall(_.isInstanceOf[ParseWarning])) Some(program)
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index 29c2138ec..e706cf048 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -89,11 +89,12 @@ trait SilFrontend extends DefaultFrontend {
   /** For testing of plugin import feature */
   def defaultPluginCount: Int = defaultPlugins.size
 
+  protected val fp = new FastParser()
 
   protected var _plugins: SilverPluginManager = SilverPluginManager(defaultPlugins match {
     case Seq() => None
     case s => Some(s.mkString(":"))
-  })(reporter, logger, _config)
+  })(reporter, logger, _config, fp)
 
   def plugins: SilverPluginManager = _plugins
 
@@ -187,7 +188,7 @@ trait SilFrontend extends DefaultFrontend {
         val list = _config.plugin.toOption ++ defaultPlugins
         if (list.isEmpty) { None } else { Some(list.mkString(":")) }
       }
-      _plugins = SilverPluginManager(plugins)(reporter, logger, _config)
+      _plugins = SilverPluginManager(plugins)(reporter, logger, _config, fp)
     }
   }
 
@@ -233,7 +234,7 @@ trait SilFrontend extends DefaultFrontend {
     val file = _inputFile.get
     _plugins.beforeParse(input, isImported = false) match {
       case Some(inputPlugin) =>
-        val result = FastParser.parse(inputPlugin, file, Some(_plugins))
+        val result = fp.parse(inputPlugin, file, Some(_plugins))
           result match {
             case Parsed.Success(e@ PProgram(_, _, _, _, _, _, _, _, err_list), _) =>
               if (err_list.isEmpty || err_list.forall(p => p.isInstanceOf[ParseWarning])) {
@@ -243,7 +244,7 @@ trait SilFrontend extends DefaultFrontend {
               else Fail(err_list)
             case fail @ Parsed.Failure(_, index, extra) =>
               val msg = fail.trace().longAggregateMsg
-              val (line, col) = LineCol(index)
+              val (line, col) = fp.lineCol.getPos(index)
               Fail(List(ParseError(s"Expected $msg", SourcePosition(file, line, col))))
             //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt)
               //? Fail(List(ParseError(s"Expected $msg", SourcePosition(file, pos(0), pos(1)))))
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 15d616c2e..e220d4cb9 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -8,13 +8,15 @@ package viper.silver.parser
 
 import java.net.URL
 import java.nio.file.{Files, Path, Paths}
+
 import viper.silver.ast.{FilePosition, LabelledOld, LineCol, NoPosition, Position, SourcePosition}
 import viper.silver.ast.utility.rewriter.{ContextA, PartialContextC, StrategyBuilder}
+import viper.silver.parser.FastParserCompanion.{LW, LeadingWhitespace}
 import viper.silver.parser.Transformer.ParseTreeDuplicationError
-import viper.silver.plugin.SilverPluginManager
+import viper.silver.plugin.{ParserPluginTemplate, SilverPluginManager}
 import viper.silver.verifier.{ParseError, ParseWarning}
 
-import scala.collection.mutable
+import scala.collection.{Set, immutable, mutable}
 
 
 case class ParseException(msg: String, pos: Position) extends Exception
@@ -23,7 +25,7 @@ case class SuffixedExpressionGenerator[E <: PExp](func: PExp => E) extends (PExp
   override def apply(v1: PExp): E = func(v1)
 }
 
-object FastParser {
+object FastParserCompanion {
   import fastparse._
 
   implicit val whitespace = {
@@ -32,6 +34,83 @@ object FastParser {
       NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
+  class LeadingWhitespace[T](val p: () => P[T]) extends AnyVal {
+    /**
+      * Using `p.lw` is shorthand for `Pass ~ p` (the same parser but with possibly leading whitespace).
+      *
+      * A parser of the form `FP(p0 ~ p1.?)` or `FP(p0 ~ p2.rep)` may return an end position which
+      * includes trailing whitespaces (incl. comments, newlines) if `p1` or `p2` fail to match (the `~` does this).
+      * Instead we would like to use `FP(p0 ~~ (Pass ~ p1).?)` or `FP(p0 ~~ (Pass ~ p2).rep)`, which avoids this issue.
+      */
+    def lw(implicit ctx: P[Any]): LW[T] = new LW(() => Pass ~ p())
+    def ~~~[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~ other.p()).asInstanceOf[P[R]]
+    def ~~~/[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~/ other.p()).asInstanceOf[P[R]]
+  }
+  /**
+    * A parser which matches leading whitespaces. See `LeadingWhitespace.lw` for more info. Can only be operated on in
+    * restricted ways (e.g. `?`, `rep`, `|` or `map`), requiring that it is eventually appened to a normal parser (of type `P[V]`).
+    *
+    * For example, the following two are equivalent:
+    * {{{FP("hello" ~~~ "world".lw.?)
+    * FP("hello" ~~ (Pass ~ "world").?)}}}
+    * The type system prevents one from erroneously writing:
+    * {{{FP("hello" ~ "world".lw.?)}}}
+    */
+  class LW[T](val p: () => P[T]) {
+    def ?[V](implicit optioner: Implicits.Optioner[T, V], ctx: P[Any]): LW[V] = new LW(() => p().?.asInstanceOf[P[V]])
+    def rep[V](implicit repeater: Implicits.Repeater[T, V], ctx: P[Any]): LW[V] = new LW(() => p().rep.asInstanceOf[P[V]])
+    def |[V >: T](other: LW[V])(implicit ctx: P[Any]): LW[V] = new LW(() => (p() | other.p()).asInstanceOf[P[V]])
+    def map[V](f: T => V): LW[V] = new LW(() => p().map(f))
+  }
+
+  val basicKeywords = immutable.Set("result",
+    // types
+    "Int", "Perm", "Bool", "Ref", "Rational",
+    // boolean constants
+    "true", "false",
+    // null
+    "null",
+    // preamble importing
+    "import",
+    // declaration keywords
+    "method", "function", "predicate", "program", "domain", "axiom", "var", "returns", "field", "define",
+    // specifications
+    "requires", "ensures", "invariant",
+    // statements
+    "fold", "unfold", "inhale", "exhale", "new", "assert", "assume", "package", "apply",
+    // control flow
+    "while", "if", "elseif", "else", "goto", "label",
+    // sequences
+    "Seq",
+    // sets and multisets
+    "Set", "Multiset", "union", "intersection", "setminus", "subset",
+    // maps
+    "Map", "range",
+    // prover hint expressions
+    "unfolding", "in", "applying",
+    // old expression
+    "old", "lhs",
+    // other expressions
+    "let",
+    // quantification
+    "forall", "exists", "forperm",
+    // permission syntax
+    "acc", "wildcard", "write", "none", "epsilon", "perm",
+    // modifiers
+    "unique")
+}
+
+class FastParser {
+  import fastparse._
+
+  implicit val whitespace = {
+    import NoWhitespace._
+    implicit ctx: ParsingRun[_] =>
+      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+  }
+
+  val lineCol = new LineCol(this)
+
   /* When importing a file from standard library, e.g. `include <inc.vpr>`, the file is expected
    * to be located in `resources/${standard_import_directory}`, e.g. `resources/import/inv.vpr`.
    */
@@ -183,43 +262,16 @@ object FastParser {
     * Function that wraps a parser to provide start and end positions if the wrapped parser succeeds.
     */
   def FP[T](t: => P[T])(implicit ctx: P[_]): P[((FilePosition, FilePosition), T)] = {
-    val startPos = LineCol(ctx.index)
+    val startPos = lineCol.getPos(ctx.index)
     val res: P[T] = t
-    val finishPos = LineCol(ctx.index)
+    val finishPos = lineCol.getPos(ctx.index)
     res.map({ parsed => ((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2)), parsed) })
   }
 
   import scala.language.implicitConversions
   implicit def LeadingWhitespaceStr(p: String)(implicit ctx: P[Any]): LeadingWhitespace[Unit] = new LeadingWhitespace(() => P(p))
   implicit def LeadingWhitespace[T](p: => P[T]) = new LeadingWhitespace(() => p)
-  class LeadingWhitespace[T](val p: () => P[T]) extends AnyVal {
-  /**
-    * Using `p.lw` is shorthand for `Pass ~ p` (the same parser but with possibly leading whitespace).
-    *
-    * A parser of the form `FP(p0 ~ p1.?)` or `FP(p0 ~ p2.rep)` may return an end position which
-    * includes trailing whitespaces (incl. comments, newlines) if `p1` or `p2` fail to match (the `~` does this).
-    * Instead we would like to use `FP(p0 ~~ (Pass ~ p1).?)` or `FP(p0 ~~ (Pass ~ p2).rep)`, which avoids this issue.
-    */
-    def lw(implicit ctx: P[Any]): LW[T] = new LW(() => Pass ~ p())
-    def ~~~[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~ other.p()).asInstanceOf[P[R]]
-    def ~~~/[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~/ other.p()).asInstanceOf[P[R]]
-  }
-  /**
-    * A parser which matches leading whitespaces. See `LeadingWhitespace.lw` for more info. Can only be operated on in
-    * restricted ways (e.g. `?`, `rep`, `|` or `map`), requiring that it is eventually appened to a normal parser (of type `P[V]`).
-    * 
-    * For example, the following two are equivalent:
-    * {{{FP("hello" ~~~ "world".lw.?)
-    * FP("hello" ~~ (Pass ~ "world").?)}}}
-    * The type system prevents one from erroneously writing:
-    * {{{FP("hello" ~ "world".lw.?)}}}
-    */
-  class LW[T](val p: () => P[T]) {
-    def ?[V](implicit optioner: Implicits.Optioner[T, V], ctx: P[Any]): LW[V] = new LW(() => p().?.asInstanceOf[P[V]])
-    def rep[V](implicit repeater: Implicits.Repeater[T, V], ctx: P[Any]): LW[V] = new LW(() => p().rep.asInstanceOf[P[V]])
-    def |[V >: T](other: LW[V])(implicit ctx: P[Any]): LW[V] = new LW(() => (p() | other.p()).asInstanceOf[P[V]])
-    def map[V](f: T => V): LW[V] = new LW(() => p().map(f))
-  }
+
 
   // Actual Parser starts from here
   def identContinues[_: P] = CharIn("0-9", "A-Z", "a-z", "$_")
@@ -264,7 +316,7 @@ object FastParser {
       case fastparse.Parsed.Success(prog, _) => prog
       case fail @ fastparse.Parsed.Failure(_, index, _) =>
         val msg = fail.trace().longMsg
-        val (line, col) = LineCol(index)
+        val (line, col) = lineCol.getPos(index)
         throw ParseException(s"Expected $msg", FilePosition(path, line, col))
     }
   }
@@ -732,41 +784,7 @@ object FastParser {
   /** The file we are currently parsing (for creating positions later). */
   def file: Path = _file
 
-  lazy val keywords = Set("result",
-    // types
-    "Int", "Perm", "Bool", "Ref", "Rational",
-    // boolean constants
-    "true", "false",
-    // null
-    "null",
-    // preamble importing
-    "import",
-    // declaration keywords
-    "method", "function", "predicate", "program", "domain", "axiom", "var", "returns", "field", "define",
-    // specifications
-    "requires", "ensures", "invariant",
-    // statements
-    "fold", "unfold", "inhale", "exhale", "new", "assert", "assume", "package", "apply",
-    // control flow
-    "while", "if", "elseif", "else", "goto", "label",
-    // sequences
-    "Seq",
-    // sets and multisets
-    "Set", "Multiset", "union", "intersection", "setminus", "subset",
-    // maps
-    "Map", "range",
-    // prover hint expressions
-    "unfolding", "in", "applying",
-    // old expression
-    "old", "lhs",
-    // other expressions
-    "let",
-    // quantification
-    "forall", "exists", "forperm",
-    // permission syntax
-    "acc", "wildcard", "write", "none", "epsilon", "perm",
-    // modifiers
-    "unique") | ParserExtension.extendedKeywords
+  lazy val keywords = FastParserCompanion.basicKeywords | ParserExtension.extendedKeywords
 
 
   // Note that `typedFapp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
@@ -1247,4 +1265,132 @@ object FastParser {
   def methodSignature[_: P] = P("method" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("returns" ~ "(" ~ formalArgList ~ ")").lw.?)
 
   def entireProgram[_: P]: P[PProgram] = P(Start ~ programDecl ~ End)
+
+
+  object ParserExtension extends ParserPluginTemplate {
+
+    import ParserPluginTemplate._
+
+    /**
+      * These private variables are the storage variables for each of the extensions.
+      * As the parser are evaluated lazily, it is possible for us to stores extra parsing sequences in these variables
+      * and after the plugins are loaded, the parsers are added to these variables and when any parser is required,
+      * can be referenced back.
+      */
+    private var _newDeclAtEnd: Option[Extension[PExtender]] = None
+    private var _newDeclAtStart: Option[Extension[PExtender]] = None
+
+    private var _newExpAtEnd: Option[Extension[PExp]] = None
+    private var _newExpAtStart: Option[Extension[PExp]] = None
+
+    private var _newStmtAtEnd: Option[Extension[PStmt]] = None
+    private var _newStmtAtStart: Option[Extension[PStmt]] = None
+
+    private var _preSpecification: Option[Extension[PExp]] = None
+    private var _postSpecification: Option[Extension[PExp]] = None
+    private var _invSpecification: Option[Extension[PExp]] = None
+
+    private var _extendedKeywords: Set[String] = Set()
+
+
+    /**
+      * For more details regarding the functionality of each of these initial parser extensions
+      * and other hooks for the parser extension, please refer to ParserPluginTemplate.scala
+      */
+    override def newDeclAtStart : Extension[PExtender] = _newDeclAtStart match {
+      case None => ParserPluginTemplate.defaultExtension
+      case Some(ext) => ext
+    }
+
+    override def newDeclAtEnd : Extension[PExtender] = _newDeclAtEnd match {
+      case None => ParserPluginTemplate.defaultExtension
+      case Some(ext) => ext
+    }
+
+    override def newStmtAtEnd : Extension[PStmt] = _newStmtAtEnd match {
+      case None => ParserPluginTemplate.defaultStmtExtension
+      case Some(ext) => ext
+    }
+
+    override def newStmtAtStart : Extension[PStmt] = _newStmtAtStart match {
+      case None => ParserPluginTemplate.defaultStmtExtension
+      case Some(ext) => ext
+    }
+
+    override def newExpAtEnd : Extension[PExp] = _newExpAtEnd match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def newExpAtStart : Extension[PExp] = _newExpAtStart match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def postSpecification : Extension[PExp] = _postSpecification match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def preSpecification : Extension[PExp] = _preSpecification match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def invSpecification : Extension[PExp] = _invSpecification match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def extendedKeywords : Set[String] = _extendedKeywords
+
+    def addNewDeclAtEnd(t: Extension[PExtender]) : Unit = _newDeclAtEnd match {
+      case None => _newDeclAtEnd = Some(t)
+      case Some(s) => _newDeclAtEnd = Some(combine(s, t))
+    }
+
+    def addNewDeclAtStart(t: Extension[PExtender]) : Unit = _newDeclAtStart match {
+      case None => _newDeclAtStart = Some(t)
+      case Some(s) => _newDeclAtStart = Some(combine(s, t))
+    }
+
+    def addNewExpAtEnd(t: Extension[PExp]) : Unit = _newExpAtEnd match {
+      case None => _newExpAtEnd = Some(t)
+      case Some(s) => _newExpAtEnd = Some(combine(s, t))
+    }
+
+    def addNewExpAtStart(t: Extension[PExp]) : Unit = _newExpAtStart match {
+      case None => _newExpAtStart = Some(t)
+      case Some(s) => _newExpAtStart = Some(combine(s, t))
+    }
+
+    def addNewStmtAtEnd(t: Extension[PStmt]) : Unit = _newStmtAtEnd match {
+      case None => _newStmtAtEnd = Some(t)
+      case Some(s) => _newStmtAtEnd = Some(combine(s, t))
+    }
+
+    def addNewStmtAtStart(t: Extension[PStmt]) : Unit = _newStmtAtStart match {
+      case None => _newStmtAtStart = Some(t)
+      case Some(s) => _newStmtAtStart = Some(combine(s, t))
+    }
+
+    def addNewPreCondition(t: Extension[PExp]) : Unit = _preSpecification match {
+      case None => _preSpecification = Some(t)
+      case Some(s) => _preSpecification = Some(combine(s, t))
+    }
+
+    def addNewPostCondition(t: Extension[PExp]) : Unit = _postSpecification match {
+      case None => _postSpecification = Some(t)
+      case Some(s) => _postSpecification = Some(combine(s, t))
+    }
+
+    def addNewInvariantCondition(t: Extension[PExp]) : Unit = _invSpecification match {
+      case None => _invSpecification = Some(t)
+      case Some(s) => _invSpecification = Some(combine(s, t))
+    }
+
+    def addNewKeywords(t : Set[String]) : Unit = {
+      _extendedKeywords ++= t
+    }
+  }
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 26595c030..a6dc49cbe 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -6,6 +6,8 @@
 
 package viper.silver.parser
 
+import java.util.concurrent.atomic.{AtomicInteger, AtomicLong}
+
 import viper.silver.ast.utility.Visitor
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder}
 import viper.silver.ast.{Exp, MagicWandOp, Member, NoPosition, Position, Stmt, Type}
@@ -264,23 +266,24 @@ object PTypeVar{
   val sep = "#"
   //TODO: do this properly
   def isFreePTVName(s : String) = s.contains(sep)
-  private var lastIndex = 0
+  private val lastIndex = new AtomicInteger(0)
   //Generate a unique fresh version of old
   def fresh(old: PDomainType) = {
     require(old.isTypeVar)
-    val freshName = getFreshName(old.domain.name)
-    lastIndex+=1
+    val ind = lastIndex.getAndIncrement()
+    val freshName = getFreshName(old.domain.name, ind)
     PTypeVar(freshName)
   }
-  private def getFreshName(name:String) = name+sep+lastIndex
+  private def getFreshName(name:String, ind: Int) = name+sep+ind
+
   def freshTypeSubstitutionPTVs(tvs : Seq[PDomainType]) : PTypeRenaming = {
     require(tvs.forall(_.isTypeVar))
     freshTypeSubstitution(tvs map (tv=>tv.domain.name))
   }
   def freshTypeSubstitution(tvns : Seq[String]) : PTypeRenaming =
     {
-      lastIndex+=1
-      new PTypeRenaming((tvns map (tv=>tv->getFreshName(tv))).toMap)
+      val ind = lastIndex.getAndIncrement()
+      new PTypeRenaming((tvns map (tv=>tv->getFreshName(tv, ind))).toMap)
     }
 }
 
@@ -1104,11 +1107,10 @@ sealed trait PScope extends PNode {
 object PScope {
   type Id = Long
 
-  private[this] var counter: Id = 0L
+  private[this] val counter = new AtomicLong(0)
 
   private def uniqueId() = {
-    val id = counter
-    counter = counter + 1
+    val id = counter.getAndIncrement()
 
     id
   }
diff --git a/src/main/scala/viper/silver/parser/ParserExtension.scala b/src/main/scala/viper/silver/parser/ParserExtension.scala
deleted file mode 100644
index fd17fd894..000000000
--- a/src/main/scala/viper/silver/parser/ParserExtension.scala
+++ /dev/null
@@ -1,137 +0,0 @@
-// This Source Code Form is subject to the terms of the Mozilla Public
-// License, v. 2.0. If a copy of the MPL was not distributed with this
-// file, You can obtain one at http://mozilla.org/MPL/2.0/.
-//
-// Copyright (c) 2011-2019 ETH Zurich.
-
-package viper.silver.parser
-
-import viper.silver.plugin._
-import scala.collection.Set
-
-object ParserExtension extends ParserPluginTemplate {
-
-  import ParserPluginTemplate._
-
-  /**
-    * These private variables are the storage variables for each of the extensions.
-    * As the parser are evaluated lazily, it is possible for us to stores extra parsing sequences in these variables
-    * and after the plugins are loaded, the parsers are added to these variables and when any parser is required,
-    * can be referenced back.
-    */
-  private var _newDeclAtEnd: Option[Extension[PExtender]] = None
-  private var _newDeclAtStart: Option[Extension[PExtender]] = None
-
-  private var _newExpAtEnd: Option[Extension[PExp]] = None
-  private var _newExpAtStart: Option[Extension[PExp]] = None
-
-  private var _newStmtAtEnd: Option[Extension[PStmt]] = None
-  private var _newStmtAtStart: Option[Extension[PStmt]] = None
-
-  private var _preSpecification: Option[Extension[PExp]] = None
-  private var _postSpecification: Option[Extension[PExp]] = None
-  private var _invSpecification: Option[Extension[PExp]] = None
-
-  private var _extendedKeywords: Set[String] = Set()
-
-
-  /**
-    * For more details regarding the functionality of each of these initial parser extensions
-    * and other hooks for the parser extension, please refer to ParserPluginTemplate.scala
-    */
-  override def newDeclAtStart : Extension[PExtender] = _newDeclAtStart match {
-    case None => ParserPluginTemplate.defaultExtension
-    case Some(ext) => ext
-  }
-
-  override def newDeclAtEnd : Extension[PExtender] = _newDeclAtEnd match {
-    case None => ParserPluginTemplate.defaultExtension
-    case Some(ext) => ext
-  }
-
-  override def newStmtAtEnd : Extension[PStmt] = _newStmtAtEnd match {
-    case None => ParserPluginTemplate.defaultStmtExtension
-    case Some(ext) => ext
-  }
-
-  override def newStmtAtStart : Extension[PStmt] = _newStmtAtStart match {
-    case None => ParserPluginTemplate.defaultStmtExtension
-    case Some(ext) => ext
-  }
-
-  override def newExpAtEnd : Extension[PExp] = _newExpAtEnd match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def newExpAtStart : Extension[PExp] = _newExpAtStart match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def postSpecification : Extension[PExp] = _postSpecification match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def preSpecification : Extension[PExp] = _preSpecification match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def invSpecification : Extension[PExp] = _invSpecification match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def extendedKeywords : Set[String] = _extendedKeywords
-
-  def addNewDeclAtEnd(t: Extension[PExtender]) : Unit = _newDeclAtEnd match {
-    case None => _newDeclAtEnd = Some(t)
-    case Some(s) => _newDeclAtEnd = Some(combine(s, t))
-  }
-
-  def addNewDeclAtStart(t: Extension[PExtender]) : Unit = _newDeclAtStart match {
-    case None => _newDeclAtStart = Some(t)
-    case Some(s) => _newDeclAtStart = Some(combine(s, t))
-  }
-
-  def addNewExpAtEnd(t: Extension[PExp]) : Unit = _newExpAtEnd match {
-    case None => _newExpAtEnd = Some(t)
-    case Some(s) => _newExpAtEnd = Some(combine(s, t))
-  }
-
-  def addNewExpAtStart(t: Extension[PExp]) : Unit = _newExpAtStart match {
-    case None => _newExpAtStart = Some(t)
-    case Some(s) => _newExpAtStart = Some(combine(s, t))
-  }
-
-  def addNewStmtAtEnd(t: Extension[PStmt]) : Unit = _newStmtAtEnd match {
-    case None => _newStmtAtEnd = Some(t)
-    case Some(s) => _newStmtAtEnd = Some(combine(s, t))
-  }
-
-  def addNewStmtAtStart(t: Extension[PStmt]) : Unit = _newStmtAtStart match {
-    case None => _newStmtAtStart = Some(t)
-    case Some(s) => _newStmtAtStart = Some(combine(s, t))
-  }
-
-  def addNewPreCondition(t: Extension[PExp]) : Unit = _preSpecification match {
-    case None => _preSpecification = Some(t)
-    case Some(s) => _preSpecification = Some(combine(s, t))
-  }
-
-  def addNewPostCondition(t: Extension[PExp]) : Unit = _postSpecification match {
-    case None => _postSpecification = Some(t)
-    case Some(s) => _postSpecification = Some(combine(s, t))
-  }
-
-  def addNewInvariantCondition(t: Extension[PExp]) : Unit = _invSpecification match {
-    case None => _invSpecification = Some(t)
-    case Some(s) => _invSpecification = Some(combine(s, t))
-  }
-
-  def addNewKeywords(t : Set[String]) : Unit = {
-    _extendedKeywords ++= t
-  }
-}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/plugin/SilverPlugin.scala b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
index e69269143..63442fced 100644
--- a/src/main/scala/viper/silver/plugin/SilverPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
@@ -9,20 +9,22 @@ package viper.silver.plugin
 import ch.qos.logback.classic.Logger
 import viper.silver.ast.Program
 import viper.silver.frontend.SilFrontendConfig
-import viper.silver.parser.PProgram
+import viper.silver.parser.{FastParser, PProgram}
 import viper.silver.reporter.Reporter
 import viper.silver.verifier.{AbstractError, VerificationResult}
 
 /** Implement this abstract class in order to give your plugin access to SilFrontend's IO:
   * 1. Reporter,
-  * 2. Logger, and
-  * 2. Command line arguments
+  * 2. Logger,
+  * 3. Command line arguments, and
+  * 4. Parser.
   * Has to be set as an explicit parameter for the plugin constructor.
   */
 trait IOAwarePlugin {
   val reporter: Reporter
   val logger: Logger
   val cmdArgs: SilFrontendConfig
+  val fp: FastParser
 }
 
 /** Trait to be extended by plugins. A plugin can change the current structure of the program under verification
diff --git a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
index 7e6cac4bb..a8cd615ce 100644
--- a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
@@ -9,7 +9,7 @@ package viper.silver.plugin
 import ch.qos.logback.classic.Logger
 import viper.silver.ast._
 import viper.silver.frontend.SilFrontendConfig
-import viper.silver.parser.PProgram
+import viper.silver.parser.{FastParser, PProgram}
 import viper.silver.reporter.Reporter
 import viper.silver.verifier.{AbstractError, VerificationResult}
 
@@ -77,10 +77,10 @@ class SilverPluginManager(val plugins: Seq[SilverPlugin]) {
 object SilverPluginManager {
 
   def apply(pluginArg: Option[String])
-           (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig): SilverPluginManager =
+           (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig, fp: FastParser): SilverPluginManager =
     pluginArg match {
       case Some(plugins) =>
-        new SilverPluginManager(resolveAll(plugins)(reporter, logger, cmdArgs))
+        new SilverPluginManager(resolveAll(plugins)(reporter, logger, cmdArgs, fp))
       case None =>
         new SilverPluginManager(Seq())
     }
@@ -88,22 +88,24 @@ object SilverPluginManager {
   def apply() = new SilverPluginManager(Seq())
 
   def resolveAll(pluginArg: String)
-                (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig): Seq[SilverPlugin] =
-    pluginArg.split(":").toSeq.map(resolve(_, reporter, logger, cmdArgs)).filter(_.isDefined).map(_.get)
+                (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig, fp: FastParser): Seq[SilverPlugin] =
+    pluginArg.split(":").toSeq.map(resolve(_, reporter, logger, cmdArgs, fp)).filter(_.isDefined).map(_.get)
 
   /** Tries to create an instance of the plugin class.
     *
-    * The plugin constructor is expected to take either zero or three arguments (as specified in [[viper.silver.plugin.IOAwarePlugin]]):
+    * The plugin constructor is expected to take either zero or four arguments (as specified in [[viper.silver.plugin.IOAwarePlugin]]):
     *  [[viper.silver.reporter.Reporter]],
     *  [[ch.qos.logback.classic.Logger]],
-    *  [[viper.silver.frontend.SilFrontendConfig]].
+    *  [[viper.silver.frontend.SilFrontendConfig]],
+    *  [[viper.silver.parser.FastParser]].
     *
     * Example plugin class declarations:
     * <pre>
     * class MyPlugin(val _reporter: Reporter,
     *                val _logger: Logger,
-    *                val _cmdArgs: SilFrontendConfig)
-    *                extends IOAwarePlugin(_reporter, _logger, _cmdArgs) with SilverPlugin
+    *                val _cmdArgs: SilFrontendConfig,
+    *                val _fp: FastParser)
+    *                extends IOAwarePlugin(_reporter, _logger, _cmdArgs, _fp) with SilverPlugin
     * </pre>
     * <pre>
     * class MyPlugin extends SilverPlugin
@@ -115,6 +117,7 @@ object SilverPluginManager {
     * @param reporter  The reporter to be used in the plugin.
     * @param logger    The logger to be used in the plugin.
     * @param cmdArgs   The config object to be accessible from the plugin.
+    * @param fp        The parser object to be used by the plugin.
     *
     * @return A fresh instance of the plugin class
     *
@@ -122,13 +125,14 @@ object SilverPluginManager {
     * @throws PluginWrongTypeException if the plugin class does not extend [[viper.silver.plugin.SilverPlugin]]
     * @throws PluginWrongArgsException if the plugin does not provide a constructor with the expected arguments.
     */
-  def resolve(clazzName: String, reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig): Option[SilverPlugin] = {
+  def resolve(clazzName: String, reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig, fp: FastParser): Option[SilverPlugin] = {
     val clazz = try {
       val constructor = Class.forName(clazzName).getConstructor(
         classOf[viper.silver.reporter.Reporter],
         classOf[ch.qos.logback.classic.Logger],
-        classOf[viper.silver.frontend.SilFrontendConfig])
-      Some(constructor.newInstance(reporter, logger, cmdArgs))
+        classOf[viper.silver.frontend.SilFrontendConfig],
+        classOf[viper.silver.parser.FastParser])
+      Some(constructor.newInstance(reporter, logger, cmdArgs, fp))
     } catch {
       case _: NoSuchMethodException =>
         try {
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 19091f525..6618ae3d7 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -9,7 +9,7 @@ package viper.silver.plugin.standard.adt
 import fastparse._
 import viper.silver.ast.Program
 import viper.silver.ast.utility.rewriter.StrategyBuilder
-import viper.silver.parser.FastParser.{FP, formalArg, idndef, idnuse, typ, whitespace}
+import viper.silver.parser.FastParserCompanion.whitespace
 import viper.silver.parser._
 import viper.silver.plugin.standard.adt.encoding.AdtEncoder
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
@@ -17,7 +17,10 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 
 class AdtPlugin(reporter: viper.silver.reporter.Reporter,
                 logger: ch.qos.logback.classic.Logger,
-                config: viper.silver.frontend.SilFrontendConfig) extends SilverPlugin with ParserPluginTemplate {
+                config: viper.silver.frontend.SilFrontendConfig,
+                fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+
+  import fp.{FP, formalArg, idndef, idnuse, typ, ParserExtension}
 
   /**
     * Keywords used to define ADT's
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index 039952d94..167508e01 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -9,17 +9,21 @@ package viper.silver.plugin.standard.predicateinstance
 import viper.silver.ast.{Domain, DomainType, ErrTrafo, FuncApp, Function, Position, PredicateAccess, PredicateAccessPredicate, Program, WildcardPerm}
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.Traverse
-import viper.silver.parser.FastParser._
 import viper.silver.parser._
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier.{ConsistencyError, Failure, Success, VerificationResult}
 import viper.silver.verifier.errors.PreconditionInAppFalse
 import fastparse._
-import viper.silver.parser.FastParser.whitespace
+import viper.silver.parser.FastParserCompanion.whitespace
 
 import scala.collection.immutable.ListMap
 
-class PredicateInstancePlugin  extends SilverPlugin with ParserPluginTemplate {
+class PredicateInstancePlugin(reporter: viper.silver.reporter.Reporter,
+                              logger: ch.qos.logback.classic.Logger,
+                              config: viper.silver.frontend.SilFrontendConfig,
+                              fp: FastParser)  extends SilverPlugin with ParserPluginTemplate {
+
+  import fp.{FP, predAcc, ParserExtension}
 
   /**
    * Syntactic marker for predicate instances
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index a9c9d5728..7164a90a4 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -9,13 +9,18 @@ package viper.silver.plugin.standard.refute
 import fastparse.P
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast._
-import viper.silver.parser.FastParser.{FP, exp, keyword, whitespace}
-import viper.silver.parser.ParserExtension
+import viper.silver.parser.FastParserCompanion.whitespace
+import viper.silver.parser.FastParser
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier._
 import viper.silver.verifier.errors.AssertFailed
 
-class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
+class RefutePlugin(reporter: viper.silver.reporter.Reporter,
+                   logger: ch.qos.logback.classic.Logger,
+                   config: viper.silver.frontend.SilFrontendConfig,
+                   fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+
+  import fp.{FP, keyword, exp, ParserExtension}
 
   /** Keyword used to define refute statements. */
   private val refuteKeyword: String = "refute"
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index af1c9a81e..ddca26499 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -9,7 +9,6 @@ package viper.silver.plugin.standard.termination
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.{SimpleContext, Strategy, StrategyBuilder}
 import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
-import viper.silver.parser.FastParser._
 import viper.silver.parser._
 import viper.silver.plugin.standard.predicateinstance.PPredicateInstance
 import viper.silver.plugin.standard.termination.transformation.Trafo
@@ -17,11 +16,13 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier.errors.AssertFailed
 import viper.silver.verifier._
 import fastparse._
-import viper.silver.parser.FastParser.whitespace
+import viper.silver.parser.FastParserCompanion.whitespace
 
 class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
                         logger: ch.qos.logback.classic.Logger,
-                        config: viper.silver.frontend.SilFrontendConfig) extends SilverPlugin with ParserPluginTemplate {
+                        config: viper.silver.frontend.SilFrontendConfig,
+                        fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+  import fp.{FP, keyword, exp, ParserExtension}
 
   private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)
 
diff --git a/src/main/scala/viper/silver/utility/SilNameGenerator.scala b/src/main/scala/viper/silver/utility/SilNameGenerator.scala
index 6e7bb2ea5..087386286 100644
--- a/src/main/scala/viper/silver/utility/SilNameGenerator.scala
+++ b/src/main/scala/viper/silver/utility/SilNameGenerator.scala
@@ -15,7 +15,7 @@ class SilNameGenerator extends DefaultNameGenerator {
   val identFirstLetter = "[a-zA-Z$_]"
   val identOtherLetterChars = "a-zA-Z0-9$_'"
   val identOtherLetter = s"[$identOtherLetterChars]"
-  val reservedNames = Consistency.reservedNames.toSet
+  val reservedNames = Consistency.reservedNames
   val separator = "_"
   val firstCharacter = identFirstLetter.r
   val otherCharacter = identOtherLetter.r
diff --git a/src/main/scala/viper/silver/verifier/ModelParser.scala b/src/main/scala/viper/silver/verifier/ModelParser.scala
index 0a8d5c7e8..01a89c5c0 100644
--- a/src/main/scala/viper/silver/verifier/ModelParser.scala
+++ b/src/main/scala/viper/silver/verifier/ModelParser.scala
@@ -1,7 +1,7 @@
 package viper.silver.verifier
 
 import fastparse._
-import viper.silver.parser.FastParser.whitespace
+import viper.silver.parser.FastParserCompanion.whitespace
 
 object ModelParser {
   // note that the dash/minus character '-' needs to be escaped by double backslashes such that it is not interpreted as a range