diff --git a/examples/concepts/cpp/Namespaces.cpp b/examples/concepts/cpp/Namespaces.cpp
index f732fd0107..b2c25d9081 100644
--- a/examples/concepts/cpp/Namespaces.cpp
+++ b/examples/concepts/cpp/Namespaces.cpp
@@ -6,7 +6,6 @@
 int x;
 
 namespace spaceA {
-	int x;
 
 	//@ context Perm(x, write);
 	//@ ensures x == 90;
@@ -28,21 +27,15 @@ namespace spaceA {
 	}
 }
 
-//@ context Perm(spaceA::x, write);
 //@ context Perm(x, write);
 int main() {
 	x = 99;
-	spaceA::x = 5;
-	//@ assert spaceA::x == 5;
   int varA = spaceA::incr();
-  //@ assert varA == 6;
-  //@ assert spaceA::x == 90;
+  //@ assert varA == 100;
+  //@ assert x == 90;
   int varB = spaceA::spaceB::incr();
   //@ assert varB == 92;
   spaceA::spaceB::doNothing();
-  int varX = spaceA::x;
-  //@ assert varX == 90;
-
-  //@ assert x == 99;
+  //@ assert x == 90;
   return 0;
 }
\ No newline at end of file
diff --git a/examples/concepts/sycl/MethodResolving.cpp b/examples/concepts/sycl/MethodResolving.cpp
index 3c01ca05be..22026a5ec4 100644
--- a/examples/concepts/sycl/MethodResolving.cpp
+++ b/examples/concepts/sycl/MethodResolving.cpp
@@ -2,13 +2,21 @@
 
 void test2() {
 	sycl::queue myQueue;
+//	sycl::handler myHandler;
 
-	sycl::event myEvent = myQueue.submit([&](sycl::handler& cgh) {
-		cgh.parallel_for(sycl::range<3>(3,3,3), // global range
-		/*@  */
+//	sycl::range<3> myRange;
+
+	sycl::event myEvent = myQueue.submit(
+	/*@ requires true; */
+	[&](sycl::handler& cgh) {
+		cgh.parallel_for(sycl::range<3>(6,4,2), // global range
+		/*@ requires it.get_id(0) > -1;  */
 		[=] (sycl::item<3> it) {
 		//[kernel code]
-			int a = it.get_id(1) + 3;
+			int a = it.get_id(0) + it.get_id(1) + it.get_id(2) + 3;
+			int b = a + 45;
+			int c = it.get_range(0);
+			int d = it.get_linear_id();
 		});
 	});
 	int b = 20;
diff --git a/res/universal/res/cpp/sycl/sycl.hpp b/res/universal/res/cpp/sycl/sycl.hpp
index cc358dbb3d..882f16dd80 100644
--- a/res/universal/res/cpp/sycl/sycl.hpp
+++ b/res/universal/res/cpp/sycl/sycl.hpp
@@ -24,6 +24,22 @@ namespace sycl {
 
   namespace item {
   	/*@ pure @*/ int get_id(int dimension);
+  	/*@ pure @*/ int get_linear_id();
+  	/*@ pure @*/ int get_range(int dimension);
+  }
+
+  namespace nd_item {
+		/*@ pure @*/ int get_global_id(int dimension);
+		/*@ pure @*/ int get_global_linear_id();
+		/*@ pure @*/ int get_global_range(int dimension);
+
+		/*@ pure @*/ int get_local_id(int dimension);
+		/*@ pure @*/ int get_local_linear_id();
+		/*@ pure @*/ int get_local_range(int dimension);
+
+		/*@ pure @*/ int get_group_id(int dimension);
+		/*@ pure @*/ int get_group_linear_id();
+		/*@ pure @*/ int get_group_range(int dimension);
   }
 
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index 1c1c32aebd..987f515d44 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -1004,7 +1004,6 @@ final class CPPLocalDeclaration[G](val decl: CPPDeclaration[G])(implicit val o:
 final class CPPFunctionDefinition[G](val contract: ApplicableContract[G], val specs: Seq[CPPDeclarationSpecifier[G]], val declarator: CPPDeclarator[G], val body: Statement[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with CPPFunctionDefinitionImpl[G] {
   var ref: Option[RefCPPGlobalDeclaration[G]] = None
 }
-final class CPPNamespaceDefinition[G](val name: String, val declarations: Seq[GlobalDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with CPPNamespaceDefinitionImpl[G]
 
 sealed trait CPPStatement[G] extends Statement[G] with CPPStatementImpl[G]
 final case class CPPDeclarationStatement[G](decl: CPPLocalDeclaration[G])(implicit val o: Origin) extends CPPStatement[G] with CPPDeclarationStatementImpl[G]
@@ -1041,10 +1040,10 @@ sealed trait SYCLClassObject[G] extends CPPExpr[G]
 final case class SYCLEvent[G](kernel: GlobalDeclaration[G])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLEventImpl[G]
 final case class SYCLQueue[G](kernels: Seq[GlobalDeclaration[G]])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLQueueImpl[G]
 final case class SYCLHandler[G](kernel: GlobalDeclaration[G])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLHandlerImpl[G]
-final case class SYCLItem[G](dimCount: Int, dimensions: Seq[Int])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLItemImpl[G]
-final case class SYCLNDItem[G](dimCount: Int, dimensions: Seq[Expr[G]])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLNDItemImpl[G]
-final case class SYCLRange[G](dimCount: Int, dimensions: Seq[Int])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLRangeImpl[G]
-final case class SYCLNDRange[G](dimCount: Int, dimensions: Seq[Expr[G]])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLNDRangeImpl[G]
+final case class SYCLItem[G](dimensions: Seq[Int])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLItemImpl[G]
+final case class SYCLNDItem[G](dimensions: Seq[Expr[G]])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLNDItemImpl[G]
+final case class SYCLRange[G](dimensions: Seq[Int])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLRangeImpl[G]
+final case class SYCLNDRange[G](dimensions: Seq[Expr[G]])(implicit val o: Origin) extends SYCLClassObject[G] with SYCLNDRangeImpl[G]
 
 sealed trait SYCLKernelDefinition[G] extends GlobalDeclaration[G]
 final case class SYCLBasicKernelDefinition[G](dimensions: Expr[G], body: GlobalDeclaration[G])(implicit val o: Origin) extends SYCLKernelDefinition[G] with SYCLBasicKernelDefinitionImpl[G]
diff --git a/src/col/vct/col/ast/lang/CPPNamespaceDefinitionImpl.scala b/src/col/vct/col/ast/lang/CPPNamespaceDefinitionImpl.scala
deleted file mode 100644
index afb2ebf8df..0000000000
--- a/src/col/vct/col/ast/lang/CPPNamespaceDefinitionImpl.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-package vct.col.ast.lang
-
-import vct.col.ast.CPPNamespaceDefinition
-import vct.col.print._
-
-trait CPPNamespaceDefinitionImpl[G] { this: CPPNamespaceDefinition[G] =>
-
-  override def layout(implicit ctx: Ctx): Doc =
-    Doc.stack(Seq(
-      Text("namespace") <+> Text(name) <+>
-      "{" <>> Doc.stack(declarations) <+/> "}"
-    ))
-}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/SYCLItemImpl.scala b/src/col/vct/col/ast/lang/SYCLItemImpl.scala
index 84e0b00e49..5bd166b491 100644
--- a/src/col/vct/col/ast/lang/SYCLItemImpl.scala
+++ b/src/col/vct/col/ast/lang/SYCLItemImpl.scala
@@ -4,9 +4,9 @@ import vct.col.ast.{SYCLItem, SYCLTItem, Type}
 import vct.col.print.{Ctx, Doc, Group, Text}
 
 trait SYCLItemImpl[G] { this: SYCLItem[G] =>
-  override def t: Type[G] = SYCLTItem(dimCount)
+  override def t: Type[G] = SYCLTItem(dimensions.size)
 
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("sycl::item") <> "<" <> Text(dimCount.toString) <> ">" <>
+    Group(Text("sycl::item") <> "<" <> Text(dimensions.size.toString) <> ">" <>
       "(" <> Text(dimensions.mkString(",")) <> ")")
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/SYCLNDItemImpl.scala b/src/col/vct/col/ast/lang/SYCLNDItemImpl.scala
index e3529546c1..e0a26fcc27 100644
--- a/src/col/vct/col/ast/lang/SYCLNDItemImpl.scala
+++ b/src/col/vct/col/ast/lang/SYCLNDItemImpl.scala
@@ -4,9 +4,9 @@ import vct.col.ast.{SYCLNDItem, SYCLTNDItem, Type}
 import vct.col.print.{Ctx, Doc, Group, Text}
 
 trait SYCLNDItemImpl[G] { this: SYCLNDItem[G] =>
-  override def t: Type[G] = SYCLTNDItem(dimCount)
+  override def t: Type[G] = SYCLTNDItem(dimensions.size)
 
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("sycl::nd_item") <> "<" <> Text(dimCount.toString) <> ">" <>
+    Group(Text("sycl::nd_item") <> "<" <> Text(dimensions.size.toString) <> ">" <>
       "(" <> Text(dimensions.map(x => x.show).mkString(",")) <> ")")
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/SYCLNDRangeImpl.scala b/src/col/vct/col/ast/lang/SYCLNDRangeImpl.scala
index 9231cbe257..c797302a65 100644
--- a/src/col/vct/col/ast/lang/SYCLNDRangeImpl.scala
+++ b/src/col/vct/col/ast/lang/SYCLNDRangeImpl.scala
@@ -4,9 +4,9 @@ import vct.col.ast.{SYCLNDRange, SYCLTNDRange, Type}
 import vct.col.print.{Ctx, Doc, Group, Text}
 
 trait SYCLNDRangeImpl[G] { this: SYCLNDRange[G] =>
-  override def t: Type[G] = SYCLTNDRange(dimCount)
+  override def t: Type[G] = SYCLTNDRange(dimensions.size)
 
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("sycl::nd_range") <> "<" <> Text(dimCount.toString) <> ">" <>
+    Group(Text("sycl::nd_range") <> "<" <> Text(dimensions.size.toString) <> ">" <>
       "(" <> Text(dimensions.map(x => x.show).mkString(",")) <> ")")
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/SYCLRangeImpl.scala b/src/col/vct/col/ast/lang/SYCLRangeImpl.scala
index 5f82f0cd81..74375da0b0 100644
--- a/src/col/vct/col/ast/lang/SYCLRangeImpl.scala
+++ b/src/col/vct/col/ast/lang/SYCLRangeImpl.scala
@@ -4,9 +4,9 @@ import vct.col.ast.{SYCLRange, SYCLTRange, Type}
 import vct.col.print.{Ctx, Doc, Group, Text}
 
 trait SYCLRangeImpl[G] { this: SYCLRange[G] =>
-  override def t: Type[G] = SYCLTRange(dimCount)
+  override def t: Type[G] = SYCLTRange(dimensions.size)
 
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("sycl::range") <> "<" <> Text(dimCount.toString) <> ">" <>
+    Group(Text("sycl::range") <> "<" <> Text(dimensions.size.toString) <> ">" <>
       "(" <> Text(dimensions.mkString(",")) <> ")")
 }
\ No newline at end of file
diff --git a/src/col/vct/col/feature/FeatureRainbow.scala b/src/col/vct/col/feature/FeatureRainbow.scala
index cc587ad439..941954c94e 100644
--- a/src/col/vct/col/feature/FeatureRainbow.scala
+++ b/src/col/vct/col/feature/FeatureRainbow.scala
@@ -226,7 +226,6 @@ class FeatureRainbow[G] {
     case node: CPPLocalDeclaration[G] => CPPSpecific
     case node: CPPLong[G] => CPPSpecific
     case node: CPPName[G] => CPPSpecific
-    case node: CPPNamespaceDefinition[G] => CPPSpecific
     case node: CPPParam[G] => CPPSpecific
     case node: CPPPrimitiveType[G] => CPPSpecific
     case node: CPPPure[G] => CPPSpecific
diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala
index 82bafb439b..2785c48962 100644
--- a/src/col/vct/col/resolve/Resolve.scala
+++ b/src/col/vct/col/resolve/Resolve.scala
@@ -325,7 +325,6 @@ case object ResolveReferences extends LazyLogging {
       ctx
         .copy(currentResult = Some(RefCPPLambdaDefinition(func)))
         .declare(CPP.paramsFromDeclarator(func.declarator) ++ scanLabels(func.body) ++ func.contract.givenArgs ++ func.contract.yieldsArgs)
-    case ns: CPPNamespaceDefinition[G] => ctx.declare(ns.declarations)
     case func: CPPGlobalDeclaration[G] =>
       if (func.decl.contract.nonEmpty && func.decl.inits.size > 1) {
         throw MultipleForwardDeclarationContractError(func)
diff --git a/src/col/vct/col/resolve/ctx/Referrable.scala b/src/col/vct/col/resolve/ctx/Referrable.scala
index 3766dd9763..c087037b6c 100644
--- a/src/col/vct/col/resolve/ctx/Referrable.scala
+++ b/src/col/vct/col/resolve/ctx/Referrable.scala
@@ -22,7 +22,6 @@ sealed trait Referrable[G] {
     case RefCPPTranslationUnit(_) => ""
     case RefCPPParam(decl) => CPP.nameFromDeclarator(decl.declarator)
     case RefCPPFunctionDefinition(decl) => CPP.nameFromDeclarator(decl.declarator)
-    case RefCPPNamespaceDefinition(decl) => decl.name
     case RefCPPGlobalDeclaration(decls, initIdx) => CPP.nameFromDeclarator(decls.decl.inits(initIdx).decl)
     case RefCPPLocalDeclaration(decls, initIdx) => CPP.nameFromDeclarator(decls.decl.inits(initIdx).decl)
     case RefJavaNamespace(_) => ""
@@ -93,7 +92,6 @@ case object Referrable {
     case decl: CPPTranslationUnit[G] => RefCPPTranslationUnit(decl)
     case decl: CPPParam[G] => RefCPPParam(decl)
     case decl: CPPFunctionDefinition[G] => RefCPPFunctionDefinition(decl)
-    case decl: CPPNamespaceDefinition[G] => RefCPPNamespaceDefinition(decl)
     case decl: CPPGlobalDeclaration[G] => return decl.decl.inits.indices.map(RefCPPGlobalDeclaration(decl, _))
     case decl: JavaNamespace[G] => RefJavaNamespace(decl)
     case decl: JavaClass[G] => RefJavaClass(decl)
@@ -212,7 +210,6 @@ case class RefCPPParam[G](decl: CPPParam[G]) extends Referrable[G] with CPPNameT
 case class RefCPPFunctionDefinition[G](decl: CPPFunctionDefinition[G]) extends Referrable[G] with CPPNameTarget[G] with CPPInvocationTarget[G] with ResultTarget[G]
 case class RefCPPLambdaDefinition[G](decl: CPPLambdaDefinition[G]) extends Referrable[G] with CPPInvocationTarget[G] with ResultTarget[G] with CPPTypeNameTarget[G] with CPPDerefTarget[G]
 case class RefCPPLambda[G](decl: CPPLambdaRef[G]) extends Referrable[G] with CPPTypeNameTarget[G] with CPPDerefTarget[G]
-case class RefCPPNamespaceDefinition[G](decl: CPPNamespaceDefinition[G]) extends Referrable[G]
 case class RefCPPGlobalDeclaration[G](decls: CPPGlobalDeclaration[G], initIdx: Int) extends Referrable[G] with CPPNameTarget[G] with CPPInvocationTarget[G] with ResultTarget[G]
 case class RefCPPLocalDeclaration[G](decls: CPPLocalDeclaration[G], initIdx: Int) extends Referrable[G] with CPPNameTarget[G]
 case class RefJavaNamespace[G](decl: JavaNamespace[G]) extends Referrable[G]
diff --git a/src/col/vct/col/resolve/lang/CPP.scala b/src/col/vct/col/resolve/lang/CPP.scala
index ca023bc76d..9def78589e 100644
--- a/src/col/vct/col/resolve/lang/CPP.scala
+++ b/src/col/vct/col/resolve/lang/CPP.scala
@@ -119,7 +119,7 @@ case object CPP {
     }
   }
 
-  def replacePotentialSYCLClassInstance[G](name: String, ctx: ReferenceResolutionContext[G]): String = {
+  def replacePotentialClassmemberName[G](name: String, ctx: ReferenceResolutionContext[G]): String = {
     if (name.contains('.') && name.count(x => x == '.') == 1) {
       // Class method, replace with SYCL equivalent
       val classVarName = name.split('.').head
@@ -145,56 +145,19 @@ case object CPP {
   }
 
   def findCPPName[G](name: String, genericArg: Option[Int], ctx: ReferenceResolutionContext[G]): Seq[CPPNameTarget[G]] = {
-    val targetName: String = replacePotentialSYCLClassInstance(name, ctx)
+    val targetName: String = replacePotentialClassmemberName(name, ctx)
 
-    var nameSeq = targetName.split("::")
-    if (nameSeq.length == 1) {
-      ctx.stack.flatten.collect {
-        case target: CPPNameTarget[G] if target.name == targetName => target
-      }
-    } else {
-      val ctxTarget: Option[RefCPPNamespaceDefinition[G]] = ctx.stack.flatten.collectFirst {
-        case namespace: RefCPPNamespaceDefinition[G] if namespace.name == nameSeq.head => namespace
-      }
-
-      ctxTarget match {
-        case Some(ref) =>
-          nameSeq = nameSeq.drop(1);
-          var foundNamespace: Option[CPPNamespaceDefinition[G]] = Some(ref.decl)
-          var returnVal: Seq[CPPNameTarget[G]] = Seq()
-          while (nameSeq.nonEmpty) {
-            if (foundNamespace.isEmpty) {
-              return Seq()
-            }
+    var targets = ctx.stack.flatten.collect {
+      case target: CPPNameTarget[G] if target.name == targetName => target
+    }
 
-            if (nameSeq.length > 1) {
-              // Look for nested namespaces
-              foundNamespace = foundNamespace.get.declarations.collectFirst {
-                case namespace: CPPNamespaceDefinition[G] if namespace.name == nameSeq.head => namespace
-              }
-            } else {
-              // Look for final nameTarget
-              returnVal = findDeclInNamespace(nameSeq.head, foundNamespace.get)
-              if (returnVal.isEmpty) {
-                returnVal = foundNamespace.get.declarations.collectFirst {
-                  case namespace: CPPNamespaceDefinition[G] if namespace.name == nameSeq.head =>
-                    findDeclInNamespace("constructor", namespace)
-                }.getOrElse(Seq())
-              }
-            }
-            nameSeq = nameSeq.drop(1)
-          }
-          returnVal
-        case None => Seq()
-      }
+    if (targets.isEmpty && !name.endsWith("::constructor")) {
+      // Not a known method, so search for constructor
+      targets = findCPPName(name + "::constructor", genericArg, ctx)
     }
+    targets
   }
 
-  def findDeclInNamespace[G](name: String, namespace: CPPNamespaceDefinition[G]): Seq[CPPNameTarget[G]] =
-    namespace.declarations.collect {
-      case funcDef: CPPFunctionDefinition[G] if getDeclaratorInfo(funcDef.declarator).name == name => RefCPPFunctionDefinition(funcDef)
-      case globalDecl: CPPGlobalDeclaration[G] if getDeclaratorInfo(globalDecl.decl.inits.head.decl).name == name => RefCPPGlobalDeclaration(globalDecl, 0)
-    }
 
   def findForwardDeclaration[G](declarator: CPPDeclarator[G], ctx: ReferenceResolutionContext[G]): Option[RefCPPGlobalDeclaration[G]] =
     ctx.stack.flatten.collectFirst {
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index faf3751a3b..f11f111b10 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -1665,8 +1665,6 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         declaration
       case definition: CPPFunctionDefinition[Pre] =>
         definition
-      case namespace: CPPNamespaceDefinition[Pre] =>
-        namespace
       case declaration: CPPGlobalDeclaration[Pre] =>
         declaration
       case namespace: JavaNamespace[Pre] =>
diff --git a/src/parsers/antlr4/LangCPPParser.g4 b/src/parsers/antlr4/LangCPPParser.g4
index cdefdb08a6..ab96d0edb7 100644
--- a/src/parsers/antlr4/LangCPPParser.g4
+++ b/src/parsers/antlr4/LangCPPParser.g4
@@ -63,7 +63,7 @@ nestedNameSpecifier:
 	| nestedNameSpecifier Template? simpleTemplateId Doublecolon;
 
 lambdaExpression:
-	lambdaIntroducer lambdaDeclarator? compoundStatement;
+	valEmbedContract? lambdaIntroducer lambdaDeclarator? compoundStatement;
 
 lambdaIntroducer: LeftBracket lambdaCapture? RightBracket;
 
diff --git a/src/parsers/vct/parsers/transform/CPPToCol.scala b/src/parsers/vct/parsers/transform/CPPToCol.scala
index 17ec67c6f9..5a49b2f22f 100644
--- a/src/parsers/vct/parsers/transform/CPPToCol.scala
+++ b/src/parsers/vct/parsers/transform/CPPToCol.scala
@@ -18,6 +18,21 @@ import scala.jdk.CollectionConverters._
 case class CPPToCol[G](override val originProvider: OriginProvider, override val blameProvider: BlameProvider, override val errors: Seq[(Token, Token, ExpectedError)])
   extends ToCol(originProvider, blameProvider, errors) {
 
+  var currentNamespacePath: Seq[String] = Seq()
+  def getPrependedNameDeclarator(declarator: CPPDeclarator[G])(implicit o: Origin): CPPDeclarator[G] = {
+    if (prependNamespace) {
+      declarator match {
+        case decl: CPPTypedFunctionDeclarator[G] => CPPTypedFunctionDeclarator[G](decl.params, decl.varargs, getPrependedNameDeclarator(decl.inner))
+        case CPPName(name) => CPPName[G]((currentNamespacePath :+ name).mkString("::"))(o)
+        case _ => declarator
+      }
+    } else {
+      declarator
+    }
+  }
+
+  var prependNamespace: Boolean = true
+
   def convert(implicit unit: TranslationUnitContext): Seq[GlobalDeclaration[G]] = unit match {
     case TranslationUnit0(maybeDeclSeq, _) => Seq(new CPPTranslationUnit(maybeDeclSeq.toSeq.flatMap(convert(_))))
   }
@@ -31,24 +46,39 @@ case class CPPToCol[G](override val originProvider: OriginProvider, override val
   def convert(implicit decl: DeclarationContext): Seq[GlobalDeclaration[G]] = decl match {
     case Declaration0(funcDecl) => Seq(convert(funcDecl))
     case Declaration1(blockDecl) => Seq(new CPPGlobalDeclaration(convert(blockDecl)))
-    case Declaration6(namespaceDecl) => Seq(convert(namespaceDecl))
+    case Declaration6(namespaceDecl) => convert(namespaceDecl)
     case Declaration7(_) => Seq()
-    case Declaration9(globalSpecDecl) => convert(globalSpecDecl)
+    case Declaration9(globalSpecDecl) => {
+      prependNamespace = false
+      val converted = convert(globalSpecDecl)
+      prependNamespace = true
+      converted
+    }
     case x => ??(x)
   }
 
   // Do not support inline and unnamed namespaces
-  def convert(implicit nsDef: NamespaceDefinitionContext): CPPNamespaceDefinition[G] = nsDef match {
-    case NamespaceDefinition0(None, _, Some(name), _, maybeBody, _) => new CPPNamespaceDefinition(convert(name), maybeBody.toSeq.flatMap(convert(_)))
+  def convert(implicit nsDef: NamespaceDefinitionContext): Seq[GlobalDeclaration[G]] = nsDef match {
+    case NamespaceDefinition0(None, _, Some(name), _, maybeBody, _) => {
+      val nameStr = convert(name)
+      currentNamespacePath = currentNamespacePath :+ nameStr
+      val result = maybeBody.toSeq.flatMap(convert(_))
+      currentNamespacePath = currentNamespacePath.dropRight(1)
+      result
+    }
     case x => ??(x)
   }
 
   // Not supporting attribute specifiers and virtual specifiers
   def convert(implicit funcDef: FunctionDefinitionContext): CPPFunctionDefinition[G] = funcDef match {
     case FunctionDefinition0(maybeContract, None, maybeDeclSpecs, declarator, None, body) =>
-      withContract(maybeContract, contract =>
-        new CPPFunctionDefinition(contract.consumeApplicableContract(blame(funcDef)), maybeDeclSpecs.toSeq.flatMap(convert(_)), convert(declarator), convert(body))(blame(funcDef))
+      val convertedDeclarator = getPrependedNameDeclarator(convert(declarator))
+      prependNamespace = false
+      val converted = withContract(maybeContract, contract =>
+        new CPPFunctionDefinition(contract.consumeApplicableContract(blame(funcDef)), maybeDeclSpecs.toSeq.flatMap(convert(_)), convertedDeclarator, convert(body))(blame(funcDef))
       )
+      prependNamespace = true
+      converted
     case x => ??(x)
   }
 
@@ -96,9 +126,15 @@ case class CPPToCol[G](override val originProvider: OriginProvider, override val
   // Not supporting attribute specifiers
   def convert(implicit simpleDecl: SimpleDeclarationContext): CPPDeclaration[G] = simpleDecl match {
     case SimpleDeclaration0(maybeContract, Some(declSpecs), maybeInits, _) =>
+      var convertedInits: Seq[CPPInit[G]] = Nil
+      if (maybeInits.isDefined) {
+        convertedInits = convert(maybeInits.get).map(init => {
+          CPPInit(getPrependedNameDeclarator(init.decl), init.init)
+        })
+      }
       withContract(maybeContract, contract =>
         new CPPDeclaration[G](contract.consumeApplicableContract(blame(simpleDecl)),
-          specs = convert(declSpecs), inits = maybeInits.map(convert(_)) getOrElse Nil)
+          specs = convert(declSpecs), inits = convertedInits)
       )
     case x => ??(x)
   }
@@ -703,8 +739,8 @@ case class CPPToCol[G](override val originProvider: OriginProvider, override val
   // Do not support lambdas without a declarator and ignore captures like [=] and [&]
   // EW TODO: add contract
   def convert(implicit lambda: LambdaExpressionContext): CPPLambdaDefinition[G] = lambda match {
-    case LambdaExpression0(_, Some(lambdaDecl), compoundStmnt) =>
-      withContract(None, contract =>
+    case LambdaExpression0(maybeContract, _, Some(lambdaDecl), compoundStmnt) =>
+      withContract(maybeContract, contract =>
         CPPLambdaDefinition(contract.consumeApplicableContract(blame(lambda)), convert(lambdaDecl), convert(compoundStmnt))(blame(lambda))
       )
     case x => ??(x)
diff --git a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
index 00a83a4590..e45f91c434 100644
--- a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
@@ -4,17 +4,22 @@ import com.typesafe.scalalogging.LazyLogging
 import hre.util.ScopedStack
 import vct.col.ast._
 import vct.col.origin._
-import vct.col.ref.Ref
+import vct.col.ref.{DirectRef, Ref}
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.CPP
 import vct.col.rewrite.lang.LangSpecificToCol.NotAValue
 import vct.col.rewrite.{Generation, Rewritten}
 import vct.col.util.AstBuildHelpers._
-import vct.col.util.SuccessionMap
+import vct.col.util.{AstBuildHelpers, SuccessionMap}
 import vct.result.VerificationError.UserError
 
 case object LangCPPToCol {
 
+  sealed abstract class KernelScopeLevel(val idName: String)
+  case class GlobalScope() extends KernelScopeLevel("GLOBAL_ID");
+  case class LocalScope() extends KernelScopeLevel("LOCAL_ID");
+  case class GroupScope() extends KernelScopeLevel("GROUP_ID");
+
   case class WrongCPPType(decl: CPPLocalDeclaration[_]) extends UserError {
     override def code: String = "wrongCPPType"
 
@@ -34,17 +39,31 @@ case object LangCPPToCol {
 
   case class KernelParFailure(kernel: CPPLambdaDefinition[_]) extends Blame[ParBlockFailure] {
     override def blame(error: ParBlockFailure): Unit = error match {
-//      case ParPredicateNotInjective(_, predicate) =>
-//        kernel.blame.blame(KernelPredicateNotInjective(kernel, predicate))
-//      case ParPreconditionFailed(_, _) =>
-//        PanicBlame("Kernel parallel block precondition cannot fail, since an identical predicate is required before.").blame(error)
-//      case ParBlockPostconditionFailed(failure, _) =>
-//        kernel.blame.blame(KernelPostconditionFailed(failure, kernel))
-//      case ParBlockMayNotThrow(_) =>
-//        PanicBlame("Please don't throw exceptions from a gpgpu kernel, it's not polite.").blame(error)
       case _ => PanicBlame("ELLEN: Implement blame!").blame(error)
     }
   }
+
+  case class MultipleKernels(decl1: Statement[_], decl2: CPPInvocation[_]) extends UserError {
+    override def code: String = "unsupportedMultipleKernels"
+
+    override def text: String = Origin.messagesInContext(Seq(
+      decl2.o -> "This kernel declaration is not allowed, as only one kernel declaration is allowed per command group, ...",
+      decl1.o -> "... and there is already a kernel declared here.",
+    ))
+  }
+
+  case class MissingKernel(decl: Statement[_]) extends UserError {
+    override def code: String = "unsupportedMissingKernel"
+
+    override def text: String = decl.o.messageInContext(s"There is no kernel declaration in this command group.")
+  }
+
+  case class WrongKernelDimensionsType(expr: Expr[_]) extends VerificationFailure {
+    override def code: String = "unexpectedKernelDimensionType"
+    override def position: String = expr.o.shortPosition
+    override def desc: String = expr.o.messageInContext("Wrong type for the dimensions parameter of the kernel. The dimensions parameter in a kernel declaration is supposed to be of type sycl::range<int> or sycl::nd_range<int>.")
+    override def inlineDesc: String = "Wrong type for the dimensions parameter, it is supposed to be of type sycl::range<int> or sycl::nd_range<int>."
+  }
 }
 
 case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
@@ -52,7 +71,6 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   type Post = Rewritten[Pre]
   implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw
 
-  val namespace: ScopedStack[CPPNamespaceDefinition[Pre]] = ScopedStack()
   val cppFunctionSuccessor: SuccessionMap[CPPFunctionDefinition[Pre], Procedure[Post]] = SuccessionMap()
   val cppFunctionDeclSuccessor: SuccessionMap[(CPPGlobalDeclaration[Pre], Int), Procedure[Post]] = SuccessionMap()
   val cppNameSuccessor: SuccessionMap[CPPNameTarget[Pre], Variable[Post]] = SuccessionMap()
@@ -60,6 +78,10 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   val cppCurrentDefinitionParamSubstitutions: ScopedStack[Map[CPPParam[Pre], CPPParam[Pre]]] = ScopedStack()
   val cppLambdaSuccessor: SuccessionMap[CPPLambdaDefinition[Pre], Procedure[Post]] = SuccessionMap()
 
+  var currentGlobalDimensions: ScopedStack[Seq[IterVariable[Pre]]] = ScopedStack()
+  var currentLocalDimensions: ScopedStack[Seq[IterVariable[Pre]]] = ScopedStack()
+  var currentGroupDimensions: ScopedStack[Seq[IterVariable[Pre]]] = ScopedStack()
+
   def rewriteUnit(cppUnit: CPPTranslationUnit[Pre]): Unit = {
     cppUnit.declarations.foreach(rw.dispatch)
   }
@@ -123,39 +145,6 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     }
   }
 
-  def rewriteLambdaDef(lambda: CPPLambdaDefinition[Pre], body: Statement[Pre]): Unit = {
-    val info = CPP.getDeclaratorInfo(lambda.declarator)
-    val returnType = TVoid[Post]()
-
-    val namedO = InterpretedOriginVariable("VERCORS_LAMBDA_METHOD", lambda.o)
-    val proc =
-      cppCurrentDefinitionParamSubstitutions.having(Map.empty) {
-        rw.globalDeclarations.declare(
-          {
-            val params = rw.variables.collect {
-              CPP.filterOutLambdaParams(info.params.get).foreach(rw.dispatch)
-            }._1
-            rw.labelDecls.scope {
-              new Procedure[Post](
-                returnType = returnType,
-                args = params,
-                outArgs = Nil,
-                typeArgs = Nil,
-                body = Some(rw.dispatch(body)),
-                contract = rw.dispatch(lambda.contract),
-              )(lambda.blame)(namedO)
-            }
-          }
-        )
-      }
-
-    cppLambdaSuccessor(lambda) = proc
-
-//    val returnExpr = new CPPLambdaRef[Post]()(namedO)
-//    returnExpr.ref = Some(new RefProcedure[Post](proc))
-//    returnExpr
-  }
-
   def rewriteGlobalDecl(decl: CPPGlobalDeclaration[Pre]): Unit = {
     val t = decl.decl.specs.collectFirst { case t: CPPSpecificationType[Pre] => rw.dispatch(t.t) }.get
     for ((init, idx) <- decl.decl.inits.zipWithIndex if init.ref.isEmpty) {
@@ -214,14 +203,6 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     }
   }
 
-  def rewriteNamespaceDef(ns: CPPNamespaceDefinition[Pre]): Unit = {
-    ns.drop()
-    namespace.having(ns) {
-      // Do not enter a scope, so methods of the namespace are declared globally to the program.
-      ns.declarations.foreach(rw.dispatch)
-    }
-  }
-
   def result(ref: RefCPPFunctionDefinition[Pre])(implicit o: Origin): Expr[Post] =
     Result[Post](cppFunctionSuccessor.ref(ref.decl))
 
@@ -304,22 +285,41 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     val RefCPPGlobalDeclaration(decls, initIdx) = e
     implicit val o: Origin = inv.o
 
-    val arg = if (args.size == 1) {
-      args.head match {
-        case IntegerValue(i) if i >= 0 && i < 3 => Some(i.toInt)
-        case _ => None
-      }
-    } else None
     // Process lambda parameters and remove them from the parameter list
     var filteredArgs = Seq[Expr[Pre]]()
     args.foreach {
       case argument: CPPLambdaDefinition[Pre] =>
       case argument => filteredArgs = filteredArgs :+ argument
     }
-    (e.name, arg) match {
+    val firstArgIntValue = if (filteredArgs.size == 1) {
+      filteredArgs.head match {
+        case IntegerValue(i) if i >= 0 && i < 3 => Some(i.toInt)
+        case _ => None
+      }
+    }
+    else None
+    (e.name, firstArgIntValue) match {
+      case ("sycl::range::constructor", _) => {
+        SYCLRange[Post](filteredArgs.map {
+          case IntegerValue(i) => i.toInt
+          case _ => -1
+        })
+      }
+      case ("sycl::item::get_id", Some(i)) => rw.dispatch(getSYCLWorkItemId(GlobalScope(), i))
+      case ("sycl::item::get_linear_id", None) => rw.dispatch(getSYCLLinearWorkItemId(GlobalScope()))
+      case ("sycl::item::get_range", Some(i)) => rw.dispatch(getSYCLWorkItemRange(GlobalScope(), i))
+      case ("sycl::nd_item::get_global_id", Some(i)) => rw.dispatch(getSYCLWorkItemId(GlobalScope(), i))
+      case ("sycl::nd_item::get_global_linear_id", None) => rw.dispatch(getSYCLLinearWorkItemId(GlobalScope()))
+      case ("sycl::nd_item::get_global_range", Some(i)) => rw.dispatch(getSYCLWorkItemRange(GlobalScope(), i))
+      case ("sycl::nd_item::get_local_id", Some(i)) => rw.dispatch(getSYCLWorkItemId(LocalScope(), i))
+      case ("sycl::nd_item::get_local_linear_id", None) => rw.dispatch(getSYCLLinearWorkItemId(GlobalScope()))
+      case ("sycl::nd_item::get_local_range", Some(i)) => rw.dispatch(getSYCLWorkItemRange(LocalScope(), i))
+      case ("sycl::nd_item::get_group_id", Some(i)) => rw.dispatch(getSYCLWorkItemId(GroupScope(), i))
+      case ("sycl::nd_item::get_group_linear_id", None) => rw.dispatch(getSYCLLinearWorkItemId(GlobalScope()))
+      case ("sycl::nd_item::get_group_range", Some(i)) => rw.dispatch(getSYCLWorkItemRange(GroupScope(), i))
+      case ("sycl::queue::submit", _) => rewriteSYCLQueueSubmit(inv)
       case _ => {
-        var procedureRef: Ref[Post, Procedure[Post]] = cppFunctionDeclSuccessor.ref((decls, initIdx))
-        procedureRef = rewritePotentialSYCLProcedure(e, procedureRef, inv)
+        val procedureRef: Ref[Post, Procedure[Post]] = cppFunctionDeclSuccessor.ref((decls, initIdx))
         ProcedureInvocation[Post](
           procedureRef, filteredArgs.map(rw.dispatch), Nil, Nil,
           givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
@@ -329,44 +329,144 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     }
   }
 
-  def rewritePotentialSYCLProcedure(declaration: RefCPPGlobalDeclaration[Pre], declProcedureRef: Ref[Post, Procedure[Post]], invocation: CPPInvocation[Pre]): Ref[Post, Procedure[Post]] = {
-    // cppLambdaSuccessor(invocation.args(0))
-    // EW TODO: better method matching
-    if (declaration.name == "submit" && CPP.getPrimitiveType(declaration.decls.decl.specs).isInstanceOf[SYCLTEvent[Pre]]) {
-      // Command group submit method
-//      val commandGroupProcedure = cppLambdaSuccessor(invocation.args.head.asInstanceOf[CPPLambdaDefinition[Pre]])
-      val lambdaDef: CPPLambdaDefinition[Pre] = invocation.args.head.asInstanceOf[CPPLambdaDefinition[Pre]]
-      rewriteLambdaDef(lambdaDef, lambdaDef.body)
-      val mew = 5;
-    } else if (declaration.name == "parallel_for" && CPP.getPrimitiveType(declaration.decls.decl.specs).isInstanceOf[TVoid[Pre]]) {
-      // Kernel parallel_for
-      val lambdaDef: CPPLambdaDefinition[Pre] = invocation.args.toSeq(1).asInstanceOf[CPPLambdaDefinition[Pre]]
-      implicit val o: Origin = lambdaDef.body.o
-      val innerBody = lambdaDef.body.asInstanceOf[Scope[Pre]].body.asInstanceOf[Block[Pre]]
-      val blockDecl = new ParBlockDecl[Pre]()
-      val UnitAccountedPredicate(contractRequires: Expr[Pre]) = lambdaDef.contract.requires
-      val UnitAccountedPredicate(contractEnsures: Expr[Pre]) = lambdaDef.contract.ensures
-      val newOuterBody = ParStatement[Pre](ParBlock[Pre](
-        decl = blockDecl,
-        iters = Seq(),
-        // Context is already inherited
-        context_everywhere = lambdaDef.contract.contextEverywhere,
-        requires = contractRequires,
-        ensures = contractEnsures,
-        content = Scope[Pre](Seq(), Block[Pre](Seq(innerBody))),
-      )(KernelParFailure(lambdaDef)))
-
-      rewriteLambdaDef(lambdaDef, newOuterBody)
-//      val kernelProcedure = cppLambdaSuccessor(invocation.args.toSeq(1).asInstanceOf[CPPLambdaDefinition[Pre]])
-//      kernelProcedure.body.get.body
-      val mew = 5;
+  def getRangeDimensions(level: KernelScopeLevel): Seq[IterVariable[Pre]] =
+    try {
+      level match {
+        case GlobalScope() => currentGlobalDimensions.top
+        case LocalScope() => currentLocalDimensions.top
+        case GroupScope() => currentGroupDimensions.top
+      }
+    } catch {
+      case _: NoSuchElementException => throw new Exception()
+    }
+
+  def getSYCLWorkItemId(level: KernelScopeLevel, index: Int)(implicit o: Origin): Expr[Pre] =
+    new Local[Pre](new DirectRef(getRangeDimensions(level)(index).variable))
+
+  def getSYCLLinearWorkItemId(level: KernelScopeLevel)(implicit o: Origin): Expr[Pre] = try {
+    val dimensions = getRangeDimensions(level)
+    // See SYCL Specification section 3.11.1 for the linearization formulas
+    dimensions match {
+      case Seq(x) => new Local[Pre](new DirectRef(x.variable))
+      case Seq(x, y) =>
+        val xRef = new Local[Pre](new DirectRef(x.variable))
+        val yRef = new Local[Pre](new DirectRef(y.variable))
+        Plus(yRef, Mult(xRef, y.to))
+      case Seq(x, y, z) =>
+        val xRef = new Local[Pre](new DirectRef(x.variable))
+        val yRef = new Local[Pre](new DirectRef(y.variable))
+        val zRef = new Local[Pre](new DirectRef(z.variable))
+        Plus(Plus(zRef, Mult(yRef, z.to)), Mult(Mult(xRef, y.to), z.to))
+    }
+  } catch {
+    case _: NoSuchElementException => throw new Exception()
+  }
+
+  def getSYCLWorkItemRange(level: KernelScopeLevel, index: Int): Expr[Pre] =
+    getRangeDimensions(level)(index).to
+
+  def createRange(scope: KernelScopeLevel, dimension_index: Int, count: Int)(implicit o: Origin): IterVariable[Pre] = {
+    if (count < 1) {
+      // EW TODO: Throw custom error
+      throw new Exception()
+    }
+    val variable = new Variable[Pre](TInt())(SourceNameOrigin(s"${scope.idName}_${dimension_index}", o))
+    new IterVariable[Pre](variable, IntegerValue(0), IntegerValue(count))
+  }
+
+  def rewriteSYCLQueueSubmit(invocation: CPPInvocation[Pre]): Expr[Post] = {
+
+    // Get the lambda describing the command group
+    val commandGroupBody: Statement[Pre] = invocation.args.head.asInstanceOf[CPPLambdaDefinition[Pre]].body
+
+    // Get the kernel declarations in the command group
+    val collectedKernelDeclarations: Seq[CPPInvocation[Pre]] = {
+      commandGroupBody.asInstanceOf[Scope[Pre]].body.asInstanceOf[Block[Pre]].statements.collect({
+        case Eval(inv) if inv.isInstanceOf[CPPInvocation[Pre]] && inv.asInstanceOf[CPPInvocation[Pre]].ref.isDefined &&
+          inv.asInstanceOf[CPPInvocation[Pre]].ref.get.name == "sycl::handler::parallel_for" =>
+          inv.asInstanceOf[CPPInvocation[Pre]]
+      })
+    }
+    // Make sure there is only one kernel definition
+    if (collectedKernelDeclarations.isEmpty){
+      throw MissingKernel(commandGroupBody)
+    } else if (collectedKernelDeclarations.size > 1) {
+      throw MultipleKernels(commandGroupBody, collectedKernelDeclarations(1))
+    }
+
+    val kernelDimensions = collectedKernelDeclarations.head.args.head
+    val kernelDeclaration = collectedKernelDeclarations.head.args(1).asInstanceOf[CPPLambdaDefinition[Pre]]
+
+    // Create a block of code based on what kind of kernel it is
+    val kernelBody = kernelDimensions.t match {
+      case primitive: CPPPrimitiveType[_] if CPP.getPrimitiveType(primitive.specifiers).isInstanceOf[SYCLTRange[_]] =>
+        createBasicKernelBody(kernelDimensions, kernelDeclaration)
+      case SYCLTRange(_) => createBasicKernelBody(kernelDimensions, kernelDeclaration)
+//      case SYCLTNDRange(_) =>
+      case _ => throw BlameUnreachable("Type mismatch", WrongKernelDimensionsType(kernelDimensions))// EW TODO implement error
+    }
+
+    // EW: Contract will be replaced with permissions for data accessors
+    // Create a contract for the method that will hold the generated kernel code
+    val methodContract = {
+      implicit val o: Origin = commandGroupBody.o
+      ApplicableContract[Pre](
+        UnitAccountedPredicate(AstBuildHelpers.foldStar(Seq())),
+        UnitAccountedPredicate(AstBuildHelpers.foldStar(Seq())),
+        AstBuildHelpers.foldStar(Seq()),
+        Seq(), Seq(), Seq(), None
+      )(kernelDeclaration.contract.blame)
     }
-    declProcedureRef
+
+    // Declare the newly generated kernel code inside a new method
+    val proc = rw.globalDeclarations.declare(
+      {
+        rw.labelDecls.scope {
+          new Procedure[Post](
+            returnType = TRef[Post](),
+            args = Seq(),
+            outArgs = Nil,
+            typeArgs = Nil,
+            body = Some(rw.dispatch(kernelBody)),
+            contract = rw.dispatch(methodContract),
+          )(kernelDeclaration.blame)(InterpretedOriginVariable("VERCORS_LAMBDA_METHOD", kernelDeclaration.o))
+        }
+      }
+    )
+
+    // Return an invocation to the new method holding the kernel code
+    ProcedureInvocation[Post](
+      new DirectRef(proc), Seq(), Nil, Nil,
+      invocation.givenArgs.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
+      invocation.yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) }
+    )(invocation.blame)(invocation.o)
+  }
+
+  // EW TODO: clean up function
+  def createBasicKernelBody(kernelDimensions: Expr[Pre], kernelDeclaration: CPPLambdaDefinition[Pre]): ParStatement[Pre] = {
+    implicit val o: Origin = kernelDeclaration.body.o
+    // Get kernel dimensions
+    // EW TODO: actually check instead of assuming it is sycl range
+    val range: SYCLRange[Post] = rw.dispatch(kernelDimensions).asInstanceOf[SYCLRange[Post]]
+
+    val iters = range.dimensions.indices.map(index => createRange(GlobalScope(), index, range.dimensions(index)))
+    currentGlobalDimensions.push(iters)
+
+    val innerBody = kernelDeclaration.body.asInstanceOf[Scope[Pre]].body.asInstanceOf[Block[Pre]]
+    val blockDecl = new ParBlockDecl[Pre]()(SourceNameOrigin("SYCL_BASIC_KERNEL", o))
+    val UnitAccountedPredicate(contractRequires: Expr[Pre]) = kernelDeclaration.contract.requires
+    val UnitAccountedPredicate(contractEnsures: Expr[Pre]) = kernelDeclaration.contract.ensures
+
+    ParStatement[Pre](ParBlock[Pre](
+      decl = blockDecl,
+      iters = iters,
+      // Context is already inherited
+      context_everywhere = kernelDeclaration.contract.contextEverywhere,
+      requires = contractRequires,
+      ensures = contractEnsures,
+      content = Scope[Pre](Seq(), Block[Pre](Seq(innerBody))),
+    )(KernelParFailure(kernelDeclaration)))
   }
-//
-//  def pointerType(t: CPPTPointer[Pre]): Type[Post] = {
-//    TPointer(rw.dispatch(t.innerType))
-//  }
 
   def arrayType(t: CPPTArray[Pre]): Type[Post] = {
     // TODO: we should not use pointer here
diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
index a8e12ed9fd..d4d31db24c 100644
--- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
@@ -69,7 +69,6 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case unit: CPPTranslationUnit[Pre] => cpp.rewriteUnit(unit)
     case cppParam: CPPParam[Pre] => cpp.rewriteParam(cppParam)
     case func: CPPFunctionDefinition[Pre] => cpp.rewriteFunctionDef(func)
-    case ns: CPPNamespaceDefinition[Pre] => cpp.rewriteNamespaceDef(ns)
     case decl: CPPGlobalDeclaration[Pre] => cpp.rewriteGlobalDecl(decl)
     case decl: CPPLocalDeclaration[Pre] => ???
 
@@ -168,7 +167,6 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
 
     case local: CPPLocal[Pre] => cpp.local(local)
     case inv: CPPInvocation[Pre] => cpp.invocation(inv)
-//    case func: CPPLambdaDefinition[Pre] => cpp.rewriteLambdaDef(func)
 
     case inv: SilverPartialADTFunctionInvocation[Pre] => silver.adtInvocation(inv)
     case map: SilverUntypedNonemptyLiteralMap[Pre] => silver.nonemptyMap(map)