diff --git a/examples/concepts/unique/arrays.c b/examples/concepts/unique/arrays.c
index d5cd108b26..0c684806c7 100644
--- a/examples/concepts/unique/arrays.c
+++ b/examples/concepts/unique/arrays.c
@@ -1,11 +1,10 @@
-
 /*@
   context_everywhere x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(&x0[i], write));
   context_everywhere x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(&x1[i], 1\2));
   context_everywhere x2 != NULL ** \pointer_length(x2) == n ** (\forall* int i; 0<=i && i<n; Perm(&x2[i], 1\2));
   ensures (\forall int i; 0<=i && i<n; x0[i] == x1[i] + x2[i] );
 @*/
-int main(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){
+int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<3> @*/ int* x2){
   /*@
     loop_invariant 0 <= j && j <= n;
     loop_invariant (\forall int i; 0<=i && i<j; x0[i] == x1[i] + x2[i] );
diff --git a/res/universal/res/adt/const_pointer.pvl b/res/universal/res/adt/const_pointer.pvl
new file mode 100644
index 0000000000..11be76c8a2
--- /dev/null
+++ b/res/universal/res/adt/const_pointer.pvl
@@ -0,0 +1,27 @@
+adt `const_pointer`<A> {
+  pure `const_pointer`<A> const_pointer_of(seq<A> b, int offset);
+  pure seq<A> const_pointer_block(`const_pointer`<A> p);
+  pure int const_pointer_offset(`const_pointer`<A> p);
+
+  // the block offset is valid wrt the length of the block
+  axiom (∀ `const_pointer`<A> p;
+    const_pointer_offset(p) >= 0 &&
+      const_pointer_offset(p) < |const_pointer_block(p)|);
+
+  // const_pointer_of is injective: a (block, offset) pair indicates a unique const_pointer value
+  axiom (∀seq<A> b, int offset;
+    {:const_pointer_block(const_pointer_of(b, offset)):} == b &&
+      {:const_pointer_offset(const_pointer_of(b, offset)):} == offset);
+}
+
+decreases;
+pure A const_ptr_deref<A>(`const_pointer`<A> p) =
+  `const_pointer`<A>.const_pointer_block(p)[`const_pointer`<A>.const_pointer_offset(p)];
+
+decreases;
+requires 0 <= `const_pointer`<A>.const_pointer_offset(p) + offset;
+requires `const_pointer`<A>.const_pointer_offset(p) + offset < |`const_pointer`<A>.const_pointer_block(p)|;
+pure `const_pointer`<A> const_ptr_add<A>(`const_pointer`<A> p, int offset) =
+  `const_pointer`<A>.const_pointer_of(
+     `const_pointer`<A>.const_pointer_block(p),
+     `const_pointer`<A>.const_pointer_offset(p) + offset);
\ 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 7f6dc8d707..5d79517d4d 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -133,6 +133,12 @@ final case class TType[G](t: Type[G])(implicit val o: Origin = DiagnosticOrigin)
 final case class TVar[G](ref: Ref[G, Variable[G]])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends Type[G] with TVarImpl[G]
+final case class TConst[G](inner: Type[G])(
+  implicit val o: Origin = DiagnosticOrigin
+) extends Type[G] with TConstImpl[G]
+final case class TUnique[G](inner: Type[G], unique: BigInt)(
+  implicit val o: Origin = DiagnosticOrigin
+) extends Type[G] with TUniqueImpl[G]
 
 sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G]
 final case class TPointer[G](element: Type[G])(
@@ -141,6 +147,9 @@ final case class TPointer[G](element: Type[G])(
 final case class TUniquePointer[G](element: Type[G], id: BigInt)(
   implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TUniquePointerImpl[G]
+final case class TConstPointer[G](pureElement: Type[G])(
+  implicit val o: Origin = DiagnosticOrigin
+) extends PointerType[G] with TConstPointerImpl[G]
 
 sealed trait CompositeType[G] extends Type[G] with CompositeTypeImpl[G]
 sealed trait SizedType[G] extends CompositeType[G] with SizedTypeImpl[G]
@@ -329,10 +338,16 @@ final case class SpecIgnoreEnd[G]()(implicit val o: Origin)
 
 sealed trait NormallyCompletingStatement[G]
     extends Statement[G] with NormallyCompletingStatementImpl[G]
+sealed trait AssignStmt[G]
+  extends NormallyCompletingStatement[G] with AssignStmtImpl[G]
 final case class Assign[G](target: Expr[G], value: Expr[G])(
     val blame: Blame[AssignFailed]
 )(implicit val o: Origin)
-    extends NormallyCompletingStatement[G] with AssignImpl[G]
+    extends AssignStmt[G] with AssignImpl[G]
+final case class AssignInitial[G](target: Expr[G], value: Expr[G])(
+  val blame: Blame[AssignFailed]
+)(implicit val o: Origin)
+  extends AssignStmt[G] with AssignInitialImpl[G]
 final case class Send[G](decl: SendDecl[G], delta: BigInt, res: Expr[G])(
     val blame: Blame[SendFailed]
 )(implicit val o: Origin)
@@ -928,6 +943,24 @@ final case class CoercionSequence[G](coercions: Seq[Coercion[G]])(
     implicit val o: Origin
 ) extends Coercion[G] with CoercionSequenceImpl[G]
 
+final case class CoerceBetweenUnique[G](sourceId: BigInt, targetId: BigInt, innerCoercion: Coercion[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceBetweenUniqueImpl[G]
+final case class CoerceToUnique[G](source: Type[G], targetId: BigInt)(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceToUniqueImpl[G]
+final case class CoerceFromUnique[G](target: Type[G], sourceId: BigInt)(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceFromUniqueImpl[G]
+
+final case class CoerceToConst[G](source: Type[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceToConstImpl[G]
+
+final case class CoerceFromConst[G](target: Type[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceFromConstImpl[G]
+
 final case class CoerceNothingSomething[G](target: Type[G])(
     implicit val o: Origin
 ) extends Coercion[G] with CoerceNothingSomethingImpl[G]
@@ -974,7 +1007,7 @@ final case class CoerceNullJavaClass[G](
     extends Coercion[G] with CoerceNullJavaClassImpl[G]
 final case class CoerceNullAnyClass[G]()(implicit val o: Origin)
     extends Coercion[G] with CoerceNullAnyClassImpl[G]
-final case class CoerceNullPointer[G](pointerElementType: Type[G])(
+final case class CoerceNullPointer[G](target: Type[G])(
     implicit val o: Origin
 ) extends Coercion[G] with CoerceNullPointerImpl[G]
 final case class CoerceNullEnum[G](targetEnum: Ref[G, Enum[G]])(
@@ -1822,10 +1855,18 @@ final case class NewArray[G](
     initialize: Boolean,
 )(val blame: Blame[ArraySizeError])(implicit val o: Origin)
     extends Expr[G] with NewArrayImpl[G]
-final case class NewPointerArray[G](element: Type[G], size: Expr[G])(
+sealed trait NewPointer[G] extends Expr[G] with NewPointerImpl[G]
+final case class NewPointerArray[G](element: Type[G], size: Expr[G], unique: Option[BigInt])(
     val blame: Blame[ArraySizeError]
 )(implicit val o: Origin)
-    extends Expr[G] with NewPointerArrayImpl[G]
+    extends NewPointer[G] with NewPointerArrayImpl[G]
+final case class NewConstPointerArray[G](element: Type[G], size: Expr[G])(
+  val blame: Blame[ArraySizeError]
+)(implicit val o: Origin)
+  extends NewPointer[G] with NewConstPointerArrayImpl[G]
+
+final case class ToUnique[G](inner: Expr[G])(implicit val o: Origin) extends Expr[G] with ToUniqueImpl[G]
+
 final case class FreePointer[G](pointer: Expr[G])(
     val blame: Blame[PointerFreeError]
 )(implicit val o: Origin)
@@ -2494,8 +2535,6 @@ final case class CPure[G]()(implicit val o: Origin)
     extends CSpecificationModifier[G] with CPureImpl[G]
 final case class CInline[G]()(implicit val o: Origin)
     extends CSpecificationModifier[G] with CInlineImpl[G]
-final case class CUnique[G](i: BigInt)(implicit val o: Origin)
-  extends CSpecificationModifier[G] with CUniqueImpl[G]
 
 sealed trait CStorageClassSpecifier[G]
     extends CDeclarationSpecifier[G] with CStorageClassSpecifierImpl[G]
@@ -2575,6 +2614,8 @@ final case class CVolatile[G]()(implicit val o: Origin)
     extends CTypeQualifier[G] with CVolatileImpl[G]
 final case class CAtomic[G]()(implicit val o: Origin)
     extends CTypeQualifier[G] with CAtomicImpl[G]
+final case class CUnique[G](i: BigInt)(implicit val o: Origin)
+  extends CTypeQualifier[G] with CUniqueImpl[G]
 
 sealed trait CFunctionSpecifier[G]
     extends CDeclarationSpecifier[G] with CFunctionSpecifierImpl[G]
@@ -2768,6 +2809,8 @@ final case class CLiteralArray[G](exprs: Seq[Expr[G]])(implicit val o: Origin)
     extends CExpr[G] with CLiteralArrayImpl[G]
 
 sealed trait CType[G] extends Type[G] with CTypeImpl[G]
+sealed trait CPointerType[G] extends CType[G] with CPointerTypeImpl[G]
+
 final case class TCInt[G]()(implicit val o: Origin = DiagnosticOrigin)
     extends IntType[G] with CType[G] with TCIntImpl[G]
 final case class TCFloat[G](exponent: Int, mantissa: Int)(
@@ -2778,11 +2821,11 @@ final case class CPrimitiveType[G](specifiers: Seq[CDeclarationSpecifier[G]])(
 ) extends CType[G] with CPrimitiveTypeImpl[G]
 final case class CTPointer[G](innerType: Type[G])(
     implicit val o: Origin = DiagnosticOrigin
-) extends CType[G] with CTPointerImpl[G]
+) extends CPointerType[G] with CTPointerImpl[G]
 final case class CTArray[G](size: Option[Expr[G]], innerType: Type[G])(
     val blame: Blame[ArraySizeError]
 )(implicit val o: Origin = DiagnosticOrigin)
-    extends CType[G] with CTArrayImpl[G]
+    extends CPointerType[G] with CTArrayImpl[G]
 final case class CTStruct[G](ref: Ref[G, CGlobalDeclaration[G]])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends CType[G] with CTStructImpl[G]
diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala
new file mode 100644
index 0000000000..0dbd690eab
--- /dev/null
+++ b/src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.expr.heap.alloc
+
+import vct.col.ast.{NewConstPointerArray, TConstPointer, Type}
+import vct.col.ast.ops.NewConstPointerArrayOps
+import vct.col.print._
+
+trait NewConstPointerArrayImpl[G] extends NewConstPointerArrayOps[G] { this: NewConstPointerArray[G] =>
+  override lazy val t: Type[G] = TConstPointer[G](element)
+}
diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala
index 18bd2bfbf8..18eff28152 100644
--- a/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala
+++ b/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala
@@ -1,14 +1,11 @@
 package vct.col.ast.expr.heap.alloc
 
-import vct.col.ast.{NewPointerArray, TPointer, Type}
+import vct.col.ast.{NewPointerArray, TPointer, TUniquePointer, Type}
 import vct.col.print._
 import vct.col.ast.ops.NewPointerArrayOps
 
 trait NewPointerArrayImpl[G] extends NewPointerArrayOps[G] {
   this: NewPointerArray[G] =>
-  override lazy val t: Type[G] = TPointer(element)
-
-  override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
-    Text("new") <+> element <> "[" <> size <> "]"
+  override lazy val t: Type[G] = unique.map(TUniquePointer[G](element,_))
+    .getOrElse(TPointer[G](element))
 }
diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala
new file mode 100644
index 0000000000..7b0e025145
--- /dev/null
+++ b/src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala
@@ -0,0 +1,16 @@
+package vct.col.ast.expr.heap.alloc
+
+import vct.col.ast.{Expr, NewPointer, Type}
+import vct.col.origin.{ArraySizeError, Blame}
+import vct.col.print._
+
+trait NewPointerImpl[G] {
+  this: NewPointer[G] =>
+  val blame: Blame[ArraySizeError]
+  val element: Type[G]
+  val size: Expr[G]
+
+  override def precedence: Int = Precedence.POSTFIX
+  override def layout(implicit ctx: Ctx): Doc =
+    Text("new") <+> element <> "[" <> size <> "]"
+}
diff --git a/src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala
new file mode 100644
index 0000000000..082a77b2ca
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceBetweenUnique, TUnique}
+import vct.col.ast.ops.CoerceBetweenUniqueOps
+import vct.col.print._
+
+trait CoerceBetweenUniqueImpl[G] extends CoerceBetweenUniqueOps[G] { this: CoerceBetweenUnique[G] =>
+  override def target = TUnique(innerCoercion.target, targetId)
+}
diff --git a/src/col/vct/col/ast/unsorted/CoerceDecreasePrecisionImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceDecreasePrecisionImpl.scala
similarity index 73%
rename from src/col/vct/col/ast/unsorted/CoerceDecreasePrecisionImpl.scala
rename to src/col/vct/col/ast/family/coercion/CoerceDecreasePrecisionImpl.scala
index c59f6f7056..98feea40b1 100644
--- a/src/col/vct/col/ast/unsorted/CoerceDecreasePrecisionImpl.scala
+++ b/src/col/vct/col/ast/family/coercion/CoerceDecreasePrecisionImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.family.coercion
 
 import vct.col.ast.CoerceDecreasePrecision
 import vct.col.ast.ops.CoerceDecreasePrecisionOps
@@ -6,5 +6,4 @@ import vct.col.print._
 
 trait CoerceDecreasePrecisionImpl[G] extends CoerceDecreasePrecisionOps[G] {
   this: CoerceDecreasePrecision[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
 }
diff --git a/src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala
new file mode 100644
index 0000000000..ce2ab38155
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceFromConst, TConst, Type}
+import vct.col.ast.ops.CoerceFromConstOps
+import vct.col.print._
+
+trait CoerceFromConstImpl[G] extends CoerceFromConstOps[G] { this: CoerceFromConst[G] =>
+  val source: Type[G] = TConst[G](target)
+}
diff --git a/src/col/vct/col/ast/family/coercion/CoerceFromUniqueImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceFromUniqueImpl.scala
new file mode 100644
index 0000000000..4dc7a5df7c
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceFromUniqueImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.CoerceFromUnique
+import vct.col.ast.ops.CoerceFromUniqueOps
+import vct.col.print._
+
+trait CoerceFromUniqueImpl[G] extends CoerceFromUniqueOps[G] { this: CoerceFromUnique[G] =>
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}
diff --git a/src/col/vct/col/ast/unsorted/CoerceIncreasePrecisionImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceIncreasePrecisionImpl.scala
similarity index 73%
rename from src/col/vct/col/ast/unsorted/CoerceIncreasePrecisionImpl.scala
rename to src/col/vct/col/ast/family/coercion/CoerceIncreasePrecisionImpl.scala
index b7ad3c115c..0c6b0212ae 100644
--- a/src/col/vct/col/ast/unsorted/CoerceIncreasePrecisionImpl.scala
+++ b/src/col/vct/col/ast/family/coercion/CoerceIncreasePrecisionImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.family.coercion
 
 import vct.col.ast.CoerceIncreasePrecision
 import vct.col.ast.ops.CoerceIncreasePrecisionOps
@@ -6,5 +6,4 @@ import vct.col.print._
 
 trait CoerceIncreasePrecisionImpl[G] extends CoerceIncreasePrecisionOps[G] {
   this: CoerceIncreasePrecision[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
 }
diff --git a/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala
index d5ac3ea93b..6069bdc884 100644
--- a/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala
+++ b/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala
@@ -1,9 +1,8 @@
 package vct.col.ast.family.coercion
 
-import vct.col.ast.{CoerceNullPointer, TPointer}
+import vct.col.ast.{CoerceNullPointer}
 import vct.col.ast.ops.CoerceNullPointerOps
 
 trait CoerceNullPointerImpl[G] extends CoerceNullPointerOps[G] {
   this: CoerceNullPointer[G] =>
-  override def target: TPointer[G] = TPointer(pointerElementType)
 }
diff --git a/src/col/vct/col/ast/family/coercion/CoerceToConstImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceToConstImpl.scala
new file mode 100644
index 0000000000..d810a94feb
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceToConstImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceToConst, TConst, Type}
+import vct.col.ast.ops.CoerceToConstOps
+import vct.col.print._
+
+trait CoerceToConstImpl[G] extends CoerceToConstOps[G] { this: CoerceToConst[G] =>
+  val target: Type[G] = TConst[G](source)
+}
diff --git a/src/col/vct/col/ast/family/coercion/CoerceToUniqueImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceToUniqueImpl.scala
new file mode 100644
index 0000000000..a8e306a7d0
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceToUniqueImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceToUnique, TUnique}
+import vct.col.ast.ops.CoerceToUniqueOps
+import vct.col.print._
+
+trait CoerceToUniqueImpl[G] extends CoerceToUniqueOps[G] { this: CoerceToUnique[G] =>
+  override def target = TUnique(source, targetId)
+}
diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala
index 738aae3fdc..19c34c3745 100644
--- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala
+++ b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala
@@ -67,6 +67,11 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] {
       case CoerceCVectorVector(_, _) => true
       case CoerceResourceResourceVal() => true
       case CoerceResourceValResource() => true
+      case CoerceFromConst(_) => true
+      case CoerceToConst(_) => true
+      case CoerceFromUnique(_, _) => true
+      case CoerceToUnique(_, _) => true
+      case CoerceBetweenUnique(_, _, inner) => inner.isPromoting
       case CoerceMapOption(inner, _, _) => inner.isPromoting
       case CoerceMapTuple(inner, _, _) => inner.forall(_.isPromoting)
       case CoerceMapEither(inner, _, _) =>
diff --git a/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala b/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala
index 3e9a24704f..3a611f82f8 100644
--- a/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala
+++ b/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala
@@ -7,5 +7,5 @@ import vct.col.print.{Ctx, Doc}
 trait CPointerDeclaratorImpl[G] extends CPointerDeclaratorOps[G] {
   this: CPointerDeclarator[G] =>
   override def layout(implicit ctx: Ctx): Doc =
-    inner.show <> Doc.fold(pointers)(_ <> _)
+    Doc.fold(pointers)(_ <> _) <> inner.show
 }
diff --git a/src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala b/src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala
new file mode 100644
index 0000000000..5e023b3746
--- /dev/null
+++ b/src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang.c
+
+import vct.col.ast.{CPointerType, Type}
+
+trait CPointerTypeImpl[G] {
+  this: CPointerType[G] =>
+
+  val innerType: Type[G]
+}
diff --git a/src/col/vct/col/ast/statement/terminal/AssignImpl.scala b/src/col/vct/col/ast/statement/terminal/AssignImpl.scala
index f8079b4e50..4470576d6c 100644
--- a/src/col/vct/col/ast/statement/terminal/AssignImpl.scala
+++ b/src/col/vct/col/ast/statement/terminal/AssignImpl.scala
@@ -1,36 +1,8 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.{Assign, EndpointName, Local}
-import vct.col.check.{CheckContext, CheckError, SeqProgEndpointAssign}
-import vct.col.print._
+import vct.col.ast.Assign
 import vct.col.ast.ops.AssignOps
+import vct.col.print._
 
-trait AssignImpl[G]
-    extends NormallyCompletingStatementImpl[G] with AssignOps[G] {
-  this: Assign[G] =>
-  override def check(context: CheckContext[G]): Seq[CheckError] =
-    super.check(context) ++
-      (target match {
-        case Local(ref) =>
-          context.checkInWriteScope(context.roScopeReason, this, ref)
-        case EndpointName(_) if context.currentChoreography.isDefined =>
-          Seq(SeqProgEndpointAssign(this))
-        case _ => Nil
-      })
-
-  def layoutAsExpr(implicit ctx: Ctx): Doc =
-    Group(
-      target.show <+>
-        (if (ctx.syntax == Ctx.Silver)
-           ":="
-         else
-           "=") <>> value
-    )
-
-  override def layout(implicit ctx: Ctx): Doc =
-    layoutAsExpr <>
-      (if (ctx.syntax == Ctx.Silver)
-         Empty
-       else
-         Text(";"))
+trait AssignImpl[G] extends AssignOps[G] { this: Assign[G] =>
 }
diff --git a/src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala b/src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala
new file mode 100644
index 0000000000..fd13a191f4
--- /dev/null
+++ b/src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.statement.terminal
+
+import vct.col.ast.AssignInitial
+import vct.col.ast.ops.AssignInitialOps
+import vct.col.print._
+
+trait AssignInitialImpl[G] extends AssignInitialOps[G] { this: AssignInitial[G] =>
+
+}
diff --git a/src/col/vct/col/ast/statement/terminal/AssignStmtImpl.scala b/src/col/vct/col/ast/statement/terminal/AssignStmtImpl.scala
new file mode 100644
index 0000000000..319891f569
--- /dev/null
+++ b/src/col/vct/col/ast/statement/terminal/AssignStmtImpl.scala
@@ -0,0 +1,41 @@
+package vct.col.ast.statement.terminal
+
+import vct.col.ast.{AssignStmt, EndpointName, Expr, Local}
+import vct.col.check.{CheckContext, CheckError, SeqProgEndpointAssign}
+import vct.col.print._
+import vct.col.origin.{Blame, AssignFailed}
+
+trait AssignStmtImpl[G]
+    extends NormallyCompletingStatementImpl[G] {
+  this: AssignStmt[G] =>
+
+  val target: Expr[G]
+  val value: Expr[G]
+  val blame: Blame[AssignFailed]
+
+  override def check(context: CheckContext[G]): Seq[CheckError] =
+    super.check(context) ++
+      (target match {
+        case Local(ref) =>
+          context.checkInWriteScope(context.roScopeReason, this, ref)
+        case EndpointName(_) if context.currentChoreography.isDefined =>
+          Seq(SeqProgEndpointAssign(this))
+        case _ => Nil
+      })
+
+  def layoutAsExpr(implicit ctx: Ctx): Doc =
+    Group(
+      target.show <+>
+        (if (ctx.syntax == Ctx.Silver)
+           ":="
+         else
+           "=") <>> value
+    )
+
+  override def layout(implicit ctx: Ctx): Doc =
+    layoutAsExpr <>
+      (if (ctx.syntax == Ctx.Silver)
+         Empty
+       else
+         Text(";"))
+}
diff --git a/src/col/vct/col/ast/type/TConstImpl.scala b/src/col/vct/col/ast/type/TConstImpl.scala
new file mode 100644
index 0000000000..2024d2d913
--- /dev/null
+++ b/src/col/vct/col/ast/type/TConstImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TConst
+import vct.col.ast.ops.TConstOps
+import vct.col.print._
+
+trait TConstImpl[G] extends TConstOps[G] { this: TConst[G] =>
+   override def layout(implicit ctx: Ctx): Doc = Text("const") <+> inner
+}
diff --git a/src/col/vct/col/ast/type/TConstPointerImpl.scala b/src/col/vct/col/ast/type/TConstPointerImpl.scala
new file mode 100644
index 0000000000..8ac8af2d45
--- /dev/null
+++ b/src/col/vct/col/ast/type/TConstPointerImpl.scala
@@ -0,0 +1,11 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.{TConstPointer, TConst, Type}
+import vct.col.ast.ops.TConstPointerOps
+import vct.col.print._
+
+trait TConstPointerImpl[G] extends TConstPointerOps[G] { this: TConstPointer[G] =>
+  val element: Type[G] = TConst[G](pureElement)
+  override def layout(implicit ctx: Ctx): Doc =
+    Text("const_pointer") <> open <> element <> close
+}
diff --git a/src/col/vct/col/ast/type/TUniqueImpl.scala b/src/col/vct/col/ast/type/TUniqueImpl.scala
new file mode 100644
index 0000000000..5f80efa8d4
--- /dev/null
+++ b/src/col/vct/col/ast/type/TUniqueImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TUnique
+import vct.col.ast.ops.TUniqueOps
+import vct.col.print._
+
+trait TUniqueImpl[G] extends TUniqueOps[G] { this: TUnique[G] =>
+   override def layout(implicit ctx: Ctx): Doc = Text("unique<") <> unique.toString <> ">" <+> inner
+}
diff --git a/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala b/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala
new file mode 100644
index 0000000000..b0027cfc17
--- /dev/null
+++ b/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala
@@ -0,0 +1,10 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.{TAny, ToUnique}
+import vct.col.ast.ops.ToUniqueOps
+import vct.col.print._
+
+trait ToUniqueImpl[G] extends ToUniqueOps[G] { this: ToUnique[G] =>
+  // Solve typing immediately in TypeQualifiersCoercion pass
+  def t: vct.col.ast.Type[G] = TAny[G]()
+}
diff --git a/src/col/vct/col/check/Check.scala b/src/col/vct/col/check/Check.scala
index 023d37aa63..5e76bdacb7 100644
--- a/src/col/vct/col/check/Check.scala
+++ b/src/col/vct/col/check/Check.scala
@@ -243,7 +243,7 @@ case class SeqProgParticipant(s: Node[_]) extends CheckError {
 case class SeqProgNoParticipant(s: Node[_]) extends CheckError {
   val subcode = "seqProgNoParticipant"
 }
-case class SeqProgEndpointAssign(a: Assign[_]) extends CheckError {
+case class SeqProgEndpointAssign(a: AssignStmt[_]) extends CheckError {
   val subcode = "seqProgEndpointAssign"
 }
 case class SeqProgInstanceMethodPure(m: InstanceMethod[_]) extends CheckError {
diff --git a/src/col/vct/col/feature/FeatureRainbow.scala b/src/col/vct/col/feature/FeatureRainbow.scala
index d960b5a188..8a11320579 100644
--- a/src/col/vct/col/feature/FeatureRainbow.scala
+++ b/src/col/vct/col/feature/FeatureRainbow.scala
@@ -33,6 +33,7 @@ class FeatureRainbow[G] {
       case node: ArrayLocation[G] => Arrays
       case node: NewArray[G] => Arrays
       case node: NewPointerArray[G] => Arrays
+      case node: NewConstPointerArray[G] => return Seq(Arrays, AxiomaticLibraryType)
       case node: ArraySubscript[G] => Arrays
       case node: Length[G] => Arrays
       case node: TArray[G] => Arrays
@@ -79,6 +80,8 @@ class FeatureRainbow[G] {
       case node: OptNoneTyped[G] => AxiomaticLibraryType
       case node: OptSomeTyped[G] => AxiomaticLibraryType
       case node: TNull[G] => AxiomaticLibraryType
+      case node: TVector[G] => AxiomaticLibraryType
+      case node: TConstPointer[G] => AxiomaticLibraryType
 
       case node: Assert[G] => BasicStatement
       case node: Assume[G] => BasicStatement
@@ -506,7 +509,6 @@ class FeatureRainbow[G] {
       case node: TBag[G] => SilverAxiomaticLibraryType
       case node: TSeq[G] => SilverAxiomaticLibraryType
       case node: TSet[G] => SilverAxiomaticLibraryType
-      case node: TVector[G] => SilverAxiomaticLibraryType
 
       case node: SilverCurFieldPerm[G] => SilverSpecific
       case node: SilverCurPredPerm[G] => SilverSpecific
diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala
index 0ba83a7534..9aa0e4f096 100644
--- a/src/col/vct/col/origin/Blame.scala
+++ b/src/col/vct/col/origin/Blame.scala
@@ -319,11 +319,14 @@ case class PostconditionFailed(
   override def inlineDescWithSource(node: String, failure: String): String =
     s"Postcondition of `$node` may not hold, since $failure."
 }
-case class TerminationMeasureFailed(
+
+sealed trait TerminationMeasureFailed extends ContractedFailure with SeqCallableFailure
+
+case class DecreaseTerminationMeasureFailed(
     applicable: ContractApplicable[_],
-    apply: Invocation[_],
+    apply: InvokingNode[_],
     measure: DecreasesClause[_],
-) extends ContractedFailure with SeqCallableFailure with VerificationFailure {
+) extends TerminationMeasureFailed {
   override def code: String = "decreasesFailed"
   override def position: String = measure.o.shortPositionText
   override def desc: String =
@@ -335,6 +338,21 @@ case class TerminationMeasureFailed(
   override def inlineDesc: String =
     s"${apply.o.inlineContextText} may not terminate, since `${measure.o.inlineContextText}` is not decreased or not bounded"
 }
+
+case class CallTerminationMeasureFailed(apply: InvokingNode[_],
+  calledMethod: AbstractMethod[_],
+  ) extends TerminationMeasureFailed {
+  override def code: String = "callDecreasesFailed"
+  override def position: String = calledMethod.o.shortPositionText
+  override def desc: String =
+    Message.messagesInContext(
+      apply.o -> "The invocation does not terminate, since ...",
+      calledMethod.o -> "... this called method may not decrease.",
+    )
+  override def inlineDesc: String =
+    s"The invocation ${apply.o.inlineContextText} may not terminate, since `${calledMethod.o.inlineContextText}` is not decreasing"
+}
+
 case class ContextEverywhereFailedInPost(
     failure: ContractFailure,
     node: ContractApplicable[_],
diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala
index 720f63286e..709c4bf10d 100644
--- a/src/col/vct/col/resolve/lang/C.scala
+++ b/src/col/vct/col/resolve/lang/C.scala
@@ -1,5 +1,6 @@
 package vct.col.resolve.lang
 
+import com.typesafe.scalalogging.LazyLogging
 import hre.util.FuncTools
 import vct.col.ast._
 import vct.col.ast.`type`.typeclass.TFloats.{C_ieee754_32bit, C_ieee754_64bit}
@@ -10,7 +11,7 @@ import vct.col.resolve.ctx._
 import vct.col.typerules.Types
 import vct.result.VerificationError.UserError
 
-case object C {
+case object C extends LazyLogging {
   implicit private val o: Origin = DiagnosticOrigin
 
   case class CTypeNotSupported(node: Option[Node[_]]) extends UserError {
@@ -66,6 +67,18 @@ case object C {
       name: String,
   )
 
+  def qualify[G](t: Type[G], q: CTypeQualifier[G]): Type[G] = {
+    q match {
+      case CConst() => TConst(t)(q.o)
+      case CUnique(i) => TUnique(t, i)(q.o)
+      case _ => throw CTypeNotSupported(Some(q))
+    }
+  }
+
+  def processPointer[G](p: CPointer[G], t: Type[G]): Type[G] = {
+    p.qualifiers.foldLeft(CTPointer[G](t)(p.o): Type[G])(qualify[G])
+  }
+
   def getDeclaratorInfo[G](decl: CDeclarator[G]): DeclaratorInfo[G] =
     decl match {
       case CPointerDeclarator(pointers, inner) =>
@@ -74,7 +87,7 @@ case object C {
           innerInfo.params,
           t =>
             innerInfo.typeOrReturnType(
-              FuncTools.repeat[Type[G]](CTPointer(_), pointers.size, t)
+              pointers.foldLeft(t)((qt, p) => processPointer(p, qt))
             ),
           innerInfo.name,
         )
@@ -82,17 +95,7 @@ case object C {
         val innerInfo = getDeclaratorInfo(inner)
         DeclaratorInfo(
           innerInfo.params,
-          t => innerInfo.typeOrReturnType(CTArray(size, t)(c.blame)),
-          innerInfo.name,
-        )
-      case CPointerDeclarator(pointers, inner) =>
-        val innerInfo = getDeclaratorInfo(inner)
-        DeclaratorInfo(
-          innerInfo.params,
-          t =>
-            innerInfo.typeOrReturnType(
-              FuncTools.repeat[Type[G]](CTPointer(_), pointers.size, t)
-            ),
+            t => CTArray(size, t)(c.blame),
           innerInfo.name,
         )
       case CTypeExtensionDeclarator(Seq(CTypeAttribute(name, Seq(size))), inner)
@@ -125,16 +128,6 @@ case object C {
         DeclaratorInfo(params = None, typeOrReturnType = (t => t), name)
     }
 
-  def getSpecs[G](
-      decl: CDeclarator[G],
-      acc: Seq[CDeclarationSpecifier[G]] = Nil,
-  ): Seq[CDeclarationSpecifier[G]] =
-    decl match {
-      case CTypeExtensionDeclarator(extensions, inner) =>
-        getSpecs(inner, acc :+ CFunctionTypeExtensionModifier(extensions))
-      case _ => acc
-    }
-
   def getTypeFromTypeDef[G](
       decl: CDeclaration[G],
       context: Option[Node[G]] = None,
@@ -142,17 +135,20 @@ case object C {
     val specs: Seq[CDeclarationSpecifier[G]] =
       decl.specs match {
         case CTypedef() +: remaining => remaining
-        case _ => ???
+        case _ => throw CTypeNotSupported(context)
       }
 
-    // Need to get specifications from the init (can only have one init as typedef), since it can contain GCC Type extensions
-    getPrimitiveType(getSpecs(decl.inits.head.decl) ++ specs, context)
+    // Need to get specifications from the init (can only have one init as typedef)
+    if(decl.inits.size != 1) throw CTypeNotSupported(context)
+    val info = getDeclaratorInfo(decl.inits.head.decl)
+    info.typeOrReturnType(getPrimitiveType(specs, context))
   }
 
   def getPrimitiveType[G](
       specs: Seq[CDeclarationSpecifier[G]],
       context: Option[Node[G]] = None,
   ): Type[G] = {
+    implicit val o: Origin = context.map(_.o).getOrElse(DiagnosticOrigin)
     val vectorSize: Option[Expr[G]] =
       specs.collect { case ext: CFunctionTypeExtensionModifier[G] =>
         ext.extensions
@@ -164,12 +160,20 @@ case object C {
         case _ => throw CTypeNotSupported(context)
       }
 
-    val filteredSpecs = specs.filter {
-      case _: CFunctionTypeExtensionModifier[G] => false; case _ => true
-    }.collect { case spec: CTypeSpecifier[G] => spec }
+    val (typeSpecs, nonTypeSpecs) = specs.filter {
+      case _: CTypeSpecifier[G] | _: CTypeQualifierDeclarationSpecifier[G] => true ; case _ => false
+    }.partition { case _: CTypeSpecifier[G] => true; case _ => false }
+
+    var unique: Option[BigInt] = None
+    var constant: Boolean = false
+    nonTypeSpecs.foreach({
+      case CTypeQualifierDeclarationSpecifier(CUnique(i)) if unique.isEmpty => unique = Some(i)
+      case CTypeQualifierDeclarationSpecifier(CConst()) => constant = true
+      case _ => throw CTypeNotSupported(context)
+    })
 
     val t: Type[G] =
-      filteredSpecs match {
+      typeSpecs match {
         case Seq(CVoid()) => TVoid()
         case Seq(CChar()) => TChar()
         case CUnsigned() +: t if INTEGER_LIKE_TYPES.contains(t) => TCInt()
@@ -189,10 +193,13 @@ case object C {
         case spec +: _ => throw CTypeNotSupported(context.orElse(Some(spec)))
         case _ => throw CTypeNotSupported(context)
       }
-    vectorSize match {
+    val res = vectorSize match {
       case None => t
       case Some(size) => CTVector(size, t)
     }
+
+    nonTypeSpecs.collect{ case CTypeQualifierDeclarationSpecifier(q) => q }
+      .foldLeft(res)(qualify[G])
   }
 
   def nameFromDeclarator(declarator: CDeclarator[_]): String =
@@ -263,30 +270,26 @@ case object C {
       case _ => t
     }
 
-  def findPointerDeref[G](
+    def findPointerDeref[G](
       obj: Expr[G],
       name: String,
       ctx: ReferenceResolutionContext[G],
       blame: Blame[BuiltinError],
   ): Option[CDerefTarget[G]] =
     stripCPrimitiveType(obj.t) match {
-      case CTPointer(innerType: TNotAValue[G]) =>
-        innerType.decl.get match {
-          case RefCStruct(decl) => getCStructDeref(decl, name)
-          case _ => None
-        }
-      case CTPointer(struct: CTStruct[G]) =>
-        getCStructDeref(struct.ref.decl, name)
-      case CTArray(_, innerType: TNotAValue[G]) =>
-        innerType.decl.get match {
-          case RefCStruct(decl) => getCStructDeref(decl, name)
-          case _ => None
-        }
-      case CTArray(_, struct: CTStruct[G]) =>
-        getCStructDeref(struct.ref.decl, name)
+      case CTPointer(t) => findStruct(t, name)
+      case CTArray(_, t) => findStruct(t, name)
       case _ => None
     }
 
+  def findStruct[G](t: Type[G], name: String): Option[CDerefTarget[G]] = t match {
+    case innerType: TNotAValue[G] => innerType.decl.get match {
+      case RefCStruct(decl) => getCStructDeref(decl, name)
+      case _ => None
+    }
+    case struct: CTStruct[G] => getCStructDeref(struct.ref.decl, name)
+  }
+
   def getCStructDeref[G](
       decl: CGlobalDeclaration[G],
       name: String,
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index dbc1bd349a..aa8b141b44 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -263,6 +263,11 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case CoerceBoolResource() => e
       case CoerceResourceResourceVal() => e
       case CoerceResourceValResource() => e
+      case CoerceFromConst(_) => e
+      case CoerceToConst(_) => e
+      case CoerceFromUnique(_, _) => e
+      case CoerceToUnique(_, _) => e
+      case CoerceBetweenUnique(_, _, _) => e
       case CoerceBoundIntFrac() => e
       case CoerceBoundIntZFrac(_) => e
       case CoerceBoundIntFloat(_, _) => e
@@ -1564,8 +1569,10 @@ abstract class CoercingRewriter[Pre <: Generation]()
         Neq(coerce(left, sharedType), coerce(right, sharedType))
       case na @ NewArray(element, dims, moreDims, initialize) =>
         NewArray(element, dims.map(int), moreDims, initialize)(na.blame)
-      case na @ NewPointerArray(element, size) =>
-        NewPointerArray(element, size)(na.blame)
+      case na @ NewPointerArray(element, size, unique) =>
+        NewPointerArray(element, size, unique)(na.blame)
+      case nca @ NewConstPointerArray(element, size) =>
+        NewConstPointerArray(element, size)(nca.blame)
       case NewObject(cls) => NewObject(cls)
       case NoPerm() => NoPerm()
       case Not(arg) => Not(bool(arg))
@@ -2146,6 +2153,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
     stat match {
       case a @ Assert(assn) => Assert(res(assn))(a.blame)
       case a @ Assign(target, value) => Assign(target, coerce(value, target.t, canCDemote = true))(a.blame)
+      case a @ AssignInitial(target, value) => AssignInitial(target, coerce(value, target.t, canCDemote = true))(a.blame)
       case Assume(assn) => Assume(bool(assn))
       case Block(statements) => Block(statements)
       case Branch(branches) =>
diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala
index f3e90b9042..fca0b8b7f0 100644
--- a/src/col/vct/col/typerules/CoercionUtils.scala
+++ b/src/col/vct/col/typerules/CoercionUtils.scala
@@ -25,7 +25,55 @@ case object CoercionUtils {
         return Some(CoerceIdentity(source))
       case (TNothing(), _) => CoerceNothingSomething(target)
       case (_, TAny()) => CoerceSomethingAny(source)
-
+      case (TUnique(source, si), TUnique(target, ti)) =>
+        val coercion = getAnyCoercion(source, target).getOrElse(return None)
+        if(si == ti) {
+          coercion
+        } else {
+          CoerceBetweenUnique(si, ti, coercion)
+        }
+      case (TUnique(source, si), target) =>
+        if(source == target) {
+          CoerceFromUnique(source, si)
+        } else {
+          val inner = getAnyCoercion(source, target).getOrElse(return None)
+          CoercionSequence(Seq(CoerceFromUnique(source, si), inner))
+        }
+      case (source, TUnique(target, ti)) =>
+        if(source == target) {
+          CoerceToUnique(target, ti)
+        } else {
+          val inner = getAnyCoercion(source, target).getOrElse(return None)
+          CoercionSequence(Seq(inner, CoerceToUnique(target, ti)))
+        }
+      case (TConst(source), TConst(target)) =>
+        getAnyCoercion(source, target).getOrElse(return None)
+      case (source, TConst(target)) =>
+        if(source == target) {
+          source match {
+            case _: TRef[G] => return None
+            case _: PrimitiveType[G] =>
+            case _: CompositeType[G] =>
+            case _ => return None
+          }
+          CoerceToConst(target)
+        } else {
+          val inner = getAnyCoercion(source, target).getOrElse(return None)
+          CoercionSequence(Seq(inner, CoerceToConst(target)))
+        }
+      case (TConst(source), target) =>
+        if(source == target) {
+          source match {
+            case _: TRef[G] => return None
+            case _: PrimitiveType[G] =>
+            case _: CompositeType[G] =>
+            case _ => return None
+          }
+          CoerceFromConst(source)
+        } else {
+          val inner = getAnyCoercion(source, target).getOrElse(return None)
+          CoercionSequence(Seq( CoerceFromConst(source), inner))
+        }
       case (TResource(), TAnyValue()) =>
         CoercionSequence(Seq(
           CoerceResourceResourceVal(),
@@ -121,9 +169,8 @@ case object CoercionUtils {
         CoerceNullClass(target, typeArgs)
       case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target)
       case (TNull(), TAnyClass()) => CoerceNullAnyClass()
-      case (TNull(), TPointer(target)) => CoerceNullPointer(target)
-      case (TNull(), TUniquePointer(target, id)) => CoerceNullPointer(target)
-      case (TNull(), CTPointer(target)) => CoerceNullPointer(target)
+      case (TNull(), target: PointerType[G]) => CoerceNullPointer(target)
+      case (TNull(), target: CPointerType[G]) => CoerceNullPointer(target)
       case (TNull(), TEnum(target)) => CoerceNullEnum(target)
 
       case (CTArray(_, innerType), TArray(element)) if element == innerType =>
@@ -215,7 +262,7 @@ case object CoercionUtils {
       case (
             source @ TClass(sourceClass, Seq()),
             target @ TClass(targetClass, Seq()),
-          ) if source.transSupportArrows.exists { case (_, supp) =>
+          ) if source.transSupportArrows().exists { case (_, supp) =>
             supp.cls.decl == targetClass.decl
           } =>
         CoerceSupports(sourceClass, targetClass)
@@ -371,6 +418,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnySeqCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySeqCoercion)
+      case t: TConst[G] =>
+        getAnySeqCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TSeq[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -379,6 +428,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnySetCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySetCoercion)
+      case t: TConst[G] =>
+        getAnySetCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TSet[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -389,6 +440,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyVectorCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyVectorCoercion)
+      case t: TConst[G] =>
+        getAnyVectorCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: CTVector[G] =>
         Some((
           CoerceCVectorVector(t.intSize, t.innerType),
@@ -407,6 +460,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBagCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBagCoercion)
+      case t: TConst[G] =>
+        getAnyBagCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TBag[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -417,6 +472,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnySizedCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySizedCoercion)
+      case t: TConst[G] =>
+        getAnySizedCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TSeq[G] => Some((CoerceIdentity(source), t))
       case t: TSet[G] => Some((CoerceIdentity(source), t))
       case t: TBag[G] => Some((CoerceIdentity(source), t))
@@ -428,16 +485,14 @@ case object CoercionUtils {
       source: Type[G]
   ): Option[(Coercion[G], PointerType[G])] =
     source match {
+      case t: TConst[G] =>
+        getAnyPointerCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyPointerCoercion)
-      case t: TPointer[G] => Some((CoerceIdentity(source), t))
-      case t: TUniquePointer[G] => Some((CoerceIdentity(source), t))
-      case t: CTPointer[G] =>
-        Some((CoerceIdentity(source), TPointer(t.innerType)))
-      case t: CTArray[G] =>
-        Some((CoerceCArrayPointer(t.innerType), TPointer(t.innerType)))
+      case t: PointerType[G] => Some((CoerceIdentity(source), t))
+      case t: CTPointer[G] => Some((CoerceIdentity(source), TPointer(t.innerType)))
+      case t: CTArray[G] => Some((CoerceCArrayPointer(t.innerType), TPointer(t.innerType)))
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyPointerCoercion)
-      case t: CPPTArray[G] =>
-        Some((CoerceCPPArrayPointer(t.innerType), TPointer(t.innerType)))
+      case t: CPPTArray[G] => Some((CoerceCPPArrayPointer(t.innerType), TPointer(t.innerType)))
       case _: TNull[G] =>
         val t = TPointer[G](TAnyValue())
         Some((CoerceNullPointer(t), t))
@@ -449,6 +504,8 @@ case object CoercionUtils {
   ): Option[(Coercion[G], CTArray[G])] =
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyCArrayCoercion)
+      case t: TConst[G] =>
+        getAnyCArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: CTArray[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -458,6 +515,8 @@ case object CoercionUtils {
   ): Option[(Coercion[G], CPPTArray[G])] =
     source match {
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyCPPArrayCoercion)
+      case t: TConst[G] =>
+        getAnyCPPArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: CPPTArray[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -468,6 +527,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyArrayCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyArrayCoercion)
+      case t: TConst[G] =>
+        getAnyArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case acc: SYCLTAccessor[G] =>
         Some((
           CoerceIdentity(source),
@@ -492,6 +553,8 @@ case object CoercionUtils {
   ): Option[(Coercion[G], TArray[G])] =
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMatrixArrayCoercion)
+      case t: TConst[G] =>
+        getAnyMatrixArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: CPPPrimitiveType[G] =>
         chainCPPCoercion(t, getAnyMatrixArrayCoercion)
       case acc: SYCLTAccessor[G] if acc.dimCount >= 2 =>
@@ -520,6 +583,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyOptionCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyOptionCoercion)
+      case t: TConst[G] =>
+        getAnyOptionCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TOption[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -528,6 +593,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMapCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMapCoercion)
+      case t: TConst[G] =>
+        getAnyMapCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TMap[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -538,6 +605,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyTupleCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyTupleCoercion)
+      case t: TConst[G] =>
+        getAnyTupleCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TTuple[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -548,6 +617,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMatrixCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMatrixCoercion)
+      case t: TConst[G] =>
+        getAnyMatrixCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TMatrix[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -558,6 +629,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyModelCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyModelCoercion)
+      case t: TConst[G] =>
+        getAnyModelCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TModel[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -568,6 +641,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyClassCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyClassCoercion)
+      case t: TConst[G] =>
+        getAnyClassCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TClass[G] => Some((CoerceIdentity(source), t))
 
       case t: TUnion[G] =>
@@ -595,6 +670,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyEitherCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyEitherCoercion)
+      case t: TConst[G] =>
+        getAnyEitherCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TEither[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -605,6 +682,8 @@ case object CoercionUtils {
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBitvecCoercion)
       case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBitvecCoercion)
+      case t: TConst[G] =>
+        getAnyBitvecCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TSmtlibBitVector[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -616,6 +695,8 @@ case object CoercionUtils {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibFloatCoercion)
       case t: CPPPrimitiveType[G] =>
         chainCPPCoercion(t, getAnySmtlibFloatCoercion)
+      case t: TConst[G] =>
+        getAnySmtlibFloatCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TSmtlibFloatingPoint[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -627,6 +708,8 @@ case object CoercionUtils {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibArrayCoercion)
       case t: CPPPrimitiveType[G] =>
         chainCPPCoercion(t, getAnySmtlibArrayCoercion)
+      case t: TConst[G] =>
+        getAnySmtlibArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TSmtlibArray[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
@@ -638,6 +721,8 @@ case object CoercionUtils {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibSeqCoercion)
       case t: CPPPrimitiveType[G] =>
         chainCPPCoercion(t, getAnySmtlibSeqCoercion)
+      case t: TConst[G] =>
+        getAnySmtlibSeqCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TSmtlibSeq[G] => Some((CoerceIdentity(source), t))
       case _ => None
     }
diff --git a/src/col/vct/col/util/AstBuildHelpers.scala b/src/col/vct/col/util/AstBuildHelpers.scala
index 24894abb69..6aadf8813a 100644
--- a/src/col/vct/col/util/AstBuildHelpers.scala
+++ b/src/col/vct/col/util/AstBuildHelpers.scala
@@ -775,6 +775,10 @@ object AstBuildHelpers {
       implicit o: Origin
   ): Assign[G] = Assign(local, value)(AssignLocalOk)
 
+  def assignInitial[G](local: Local[G], value: Expr[G])(
+    implicit o: Origin
+  ): AssignInitial[G] = AssignInitial(local, value)(AssignLocalOk)
+
   def assignField[G](
       obj: Expr[G],
       field: Ref[G, InstanceField[G]],
diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index a9d1230ccd..7ae9b723e2 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -18,39 +18,15 @@ import vct.rewrite.lang.NoSupportSelfLoop
 import vct.col.rewrite.veymont.StructureCheck
 import vct.importer.{PathAdtImporter, Util}
 import vct.main.Main.TemporarilyUnsupported
-import vct.main.stages.Transformation.{
-  PassEventHandler,
-  TransformationCheckError,
-}
+import vct.main.stages.Transformation.{PassEventHandler, TransformationCheckError}
 import vct.options.Options
 import vct.options.types.{Backend, PathOrStd}
 import vct.resources.Resources
 import vct.result.VerificationError.SystemError
 import vct.rewrite.adt.ImportSetCompat
-import vct.rewrite.{
-  EncodeAutoValue,
-  EncodeRange,
-  EncodeResourceValues,
-  ExplicitResourceValues,
-  HeapVariableToRef,
-  MonomorphizeClass,
-  SmtlibToProverTypes,
-}
+import vct.rewrite.{TypeQualifierCoercion, EncodeAutoValue, EncodeRange, EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef, MonomorphizeClass, SmtlibToProverTypes}
 import vct.rewrite.lang.ReplaceSYCLTypes
-import vct.rewrite.veymont.{
-  DeduplicateChorGuards,
-  DropChorExpr,
-  EncodeChannels,
-  EncodeChorBranchUnanimity,
-  EncodeChoreography,
-  EncodeEndpointInequalities,
-  StratifyUnpointedExpressions,
-  GenerateChoreographyPermissions,
-  GenerateImplementation,
-  InferEndpointContexts,
-  SpecializeEndpointClasses,
-  StratifyExpressions,
-}
+import vct.rewrite.veymont.{DeduplicateChorGuards, DropChorExpr, EncodeChannels, EncodeChorBranchUnanimity, EncodeChoreography, EncodeEndpointInequalities, GenerateChoreographyPermissions, GenerateImplementation, InferEndpointContexts, SpecializeEndpointClasses, StratifyExpressions, StratifyUnpointedExpressions}
 
 import java.nio.file.Path
 import java.nio.file.Files
@@ -298,6 +274,7 @@ case class SilverTransformation(
       Seq(
         // Replace leftover SYCL types
         ReplaceSYCLTypes,
+        TypeQualifierCoercion,
         CFloatIntCoercion,
         ComputeBipGlue,
         InstantiateBipSynchronizations,
@@ -394,6 +371,7 @@ case class SilverTransformation(
         SmtlibToProverTypes,
         EnumToDomain,
         ImportArray.withArg(adtImporter),
+        ImportConstPointer.withArg(adtImporter),
         ImportPointer.withArg(adtImporter),
         ImportVector.withArg(adtImporter),
         ImportMapCompat.withArg(adtImporter),
diff --git a/src/parsers/antlr4/LangCParser.g4 b/src/parsers/antlr4/LangCParser.g4
index 932907f78d..c3951de2a0 100644
--- a/src/parsers/antlr4/LangCParser.g4
+++ b/src/parsers/antlr4/LangCParser.g4
@@ -355,6 +355,7 @@ typeQualifier
     |   'restrict'
     |   'volatile'
     |   '_Atomic'
+    |   valEmbedTypeQualifier
     ;
 
 functionSpecifier
diff --git a/src/parsers/antlr4/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4
index b1351d8e48..cadae5d5eb 100644
--- a/src/parsers/antlr4/SpecParser.g4
+++ b/src/parsers/antlr4/SpecParser.g4
@@ -417,9 +417,12 @@ valImpureDef
 valModifier
  : ('pure' | 'inline' | 'thread_local' | 'bip_annotation')
  | langStatic # valStatic
- | 'unique' '<' langConstInt '>' # valUnique
  ;
 
+valTypeQualifier
+  : 'unique' '<' langConstInt '>' # valUnique
+  ;
+
 valArgList
  : valArg
  | valArg ',' valArgList
@@ -462,3 +465,8 @@ valEmbedModifier
  : startSpec valModifier endSpec
  | {specLevel>0}? valModifier
  ;
+
+ valEmbedTypeQualifier
+  : startSpec valTypeQualifier endSpec
+  | {specLevel>0}? valTypeQualifier
+  ;
diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala
index 1f1f16a891..4947110468 100644
--- a/src/parsers/vct/parsers/transform/CToCol.scala
+++ b/src/parsers/vct/parsers/transform/CToCol.scala
@@ -168,13 +168,10 @@ case class CToCol[G](
             else if (m.consume(m.inline))
               CInline[G]()
             else
-              m.consume(m.unique).map(CUnique[G](_)).getOrElse(
-
               fail(
                 m.nodes.head,
                 "This modifier cannot be attached to a declaration in C",
               )
-              )
           },
         )
     }
@@ -293,6 +290,7 @@ case class CToCol[G](
       case TypeQualifier1(_) => CRestrict()
       case TypeQualifier2(_) => CVolatile()
       case TypeQualifier3(_) => CAtomic()
+      case TypeQualifier4(spec) => convert(spec)
     }
 
   def convert(
@@ -841,7 +839,9 @@ case class CToCol[G](
       case SpecifierQualifierList0(t, tail) =>
         convert(t) +: tail.map((e: SpecifierQualifierListContext) => convert(e))
           .getOrElse(Nil)
-      case SpecifierQualifierList1(_, _) => ??(specifiers)
+      case SpecifierQualifierList1(t, tail) =>
+        CTypeQualifierDeclarationSpecifier(convert(t)) +: tail.map((e: SpecifierQualifierListContext) => convert(e))
+        .getOrElse(Nil)
     }
 
   def convert(implicit expr: CastExpressionContext): Expr[G] =
@@ -1186,7 +1186,17 @@ case class CToCol[G](
           case "thread_local" => collector.threadLocal += mod
         }
       case ValStatic(_) => collector.static += mod
-      case ValUnique(_, _, i, _) => collector.unique += ((mod, convert(i)))
+    }
+
+  def convert(mod: ValEmbedTypeQualifierContext): CUnique[G] =
+    mod match {
+      case ValEmbedTypeQualifier0(_, mod, _) => convert(mod)
+      case ValEmbedTypeQualifier1(mod) => convert(mod)
+    }
+
+  def convert(implicit mod: ValTypeQualifierContext): CUnique[G] =
+    mod match {
+      case ValUnique(_, _, uniqueId, _) => CUnique[G](convert(uniqueId))
     }
 
   def convertEmbedWith(
diff --git a/src/parsers/vct/parsers/transform/ToCol.scala b/src/parsers/vct/parsers/transform/ToCol.scala
index e9a6a45653..e2861443a7 100644
--- a/src/parsers/vct/parsers/transform/ToCol.scala
+++ b/src/parsers/vct/parsers/transform/ToCol.scala
@@ -130,8 +130,6 @@ abstract class ToCol[G](
     val static: mutable.ArrayBuffer[ParserRuleContext] = mutable.ArrayBuffer()
     val bipAnnotation: mutable.ArrayBuffer[ParserRuleContext] = mutable
       .ArrayBuffer()
-    val unique: mutable.ArrayBuffer[(ParserRuleContext, BigInt)] = mutable
-      .ArrayBuffer()
 
     def consume(buffer: mutable.ArrayBuffer[ParserRuleContext]): Boolean = {
       val result = buffer.nonEmpty
@@ -139,13 +137,6 @@ abstract class ToCol[G](
       result
     }
 
-    def consume(buffer: mutable.ArrayBuffer[(ParserRuleContext, BigInt)]): Option[BigInt] = {
-      buffer match {
-        case mutable.ArrayBuffer() => None
-        case (_, i) +: _ => buffer.clear(); Some(i)
-      }
-    }
-
     def nodes: Seq[ParserRuleContext] =
       Seq(pure, inline, threadLocal, static, bipAnnotation).flatten
   }
diff --git a/src/rewrite/vct/rewrite/EncodeArrayValues.scala b/src/rewrite/vct/rewrite/EncodeArrayValues.scala
index dcb8e47ab8..721c13f814 100644
--- a/src/rewrite/vct/rewrite/EncodeArrayValues.scala
+++ b/src/rewrite/vct/rewrite/EncodeArrayValues.scala
@@ -60,7 +60,7 @@ case object EncodeArrayValues extends RewriterBuilder {
       }
   }
 
-  case class PointerArrayCreationFailed(arr: NewPointerArray[_])
+  case class PointerArrayCreationFailed(arr: NewPointer[_])
       extends Blame[InvocationFailure] {
     override def blame(error: InvocationFailure): Unit =
       error match {
@@ -104,7 +104,10 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
       : mutable.Map[(Type[Pre], Int, Int, Boolean), Procedure[Post]] = mutable
     .Map()
 
-  val pointerArrayCreationMethods: mutable.Map[Type[Pre], Procedure[Post]] =
+  val pointerArrayCreationMethods: mutable.Map[(Type[Pre], Option[BigInt]), Procedure[Post]] =
+    mutable.Map()
+
+  val constPointerArrayCreationMethods: mutable.Map[Type[Pre], Procedure[Post]] =
     mutable.Map()
 
   val freeMethods: mutable.Map[Type[
@@ -399,6 +402,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         args = dimArgs,
         requires = UnitAccountedPredicate(requires),
         ensures = UnitAccountedPredicate(ensures),
+        decreases = Some(DecreasesClauseNoRecursion[Post]())
       )(o.where(name =
         if (initialize)
           "make_array_initialized"
@@ -504,7 +508,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
       case _ => false
     }
 
-  def makePointerCreationMethodFor(elementType: Type[Pre]) = {
+  def makePointerCreationMethodFor(elementType: Type[Pre], unique: Option[BigInt], isConst: Boolean) = {
     implicit val o: Origin = arrayCreationOrigin
     // ar != null
     // ar.length == dim0
@@ -533,14 +537,16 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         (PointerBlockLength(result)(FramedPtrBlockLength) === sizeArg.get) &*
         (PointerBlockOffset(result)(FramedPtrBlockOffset) === zero)
       // Pointer location needs pointer add, not pointer subscript
-      ensures =
-        ensures &* makeStruct.makePerm(
-          i =>
-            PointerLocation(PointerAdd(result, i.get)(FramedPtrOffset))(
-              FramedPtrOffset
-            ),
-          IteratedPtrInjective,
-        )
+      if(!isConst) {
+        ensures =
+          ensures &* makeStruct.makePerm(
+            i =>
+              PointerLocation(PointerAdd(result, i.get)(FramedPtrOffset))(
+                FramedPtrOffset
+              ),
+            IteratedPtrInjective,
+          )
+      }
       ensures =
         if (!typeIsRef(elementType))
           ensures
@@ -557,15 +563,22 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
           ensures
         else
           ensures &* foldStar(permFields.map(_._1))
-
+      val newElementType = dispatch(elementType)
+      val returnT = {
+        if(isConst) TConstPointer(newElementType)
+        else unique.map(TUniquePointer(newElementType, _)).getOrElse(TPointer(newElementType))
+      }
+      val name = if(isConst)"make_const_pointer_array_" + elementType.toString
+        else "make_pointer_array_" + elementType.toString
       procedure(
         blame = AbstractApplicable,
         contractBlame = TrueSatisfiable,
-        returnType = TPointer(dispatch(elementType)),
+        returnType = returnT,
         args = Seq(sizeArg),
         requires = UnitAccountedPredicate(requires),
         ensures = UnitAccountedPredicate(ensures),
-      )(o.where(name = "make_pointer_array_" + elementType.toString))
+        decreases = Some(DecreasesClauseNoRecursion[Post]())
+      )(o.where(name = name))
     }))
   }
 
@@ -596,9 +609,9 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
           Nil,
           Nil,
         )(ArrayCreationFailed(newArr))
-      case newPointerArr @ NewPointerArray(element, size) =>
+      case newPointerArr @ NewPointerArray(element, size, unique) =>
         val method = pointerArrayCreationMethods
-          .getOrElseUpdate(element, makePointerCreationMethodFor(element))
+          .getOrElseUpdate((element, unique), makePointerCreationMethodFor(element, unique, false))
         ProcedureInvocation[Post](
           method.ref,
           Seq(dispatch(size)),
@@ -607,6 +620,17 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
           Nil,
           Nil,
         )(PointerArrayCreationFailed(newPointerArr))
+      case ncpa @ NewConstPointerArray(element, size) =>
+        val method = constPointerArrayCreationMethods
+          .getOrElseUpdate((element), makePointerCreationMethodFor(element, None, true))
+        ProcedureInvocation[Post](
+          method.ref,
+          Seq(dispatch(size)),
+          Nil,
+          Nil,
+          Nil,
+          Nil,
+        )(PointerArrayCreationFailed(ncpa))
       case free @ FreePointer(xs) =>
         val newXs = dispatch(xs)
         val TPointer(t) = newXs.t
diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
index 584f634c15..9c3cc66690 100644
--- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
+++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
@@ -542,6 +542,8 @@ case class ResolveExpressionSideEffects[Pre <: Generation]()
           ArraySubscript[Post](notInlined(arr), notInlined(index))(
             SubscriptAssignTarget
           )(target.o)
+        case PointerSubscript(arr, index) if arr.t.isInstanceOf[TConstPointer[_]] =>
+          throw DisallowedAssignmentTarget(target)
         case PointerSubscript(arr, index) =>
           PointerSubscript[Post](notInlined(arr), notInlined(index))(
             SubscriptAssignTarget
diff --git a/src/rewrite/vct/rewrite/TrivialAddrOf.scala b/src/rewrite/vct/rewrite/TrivialAddrOf.scala
index edc400f193..84026cf2ad 100644
--- a/src/rewrite/vct/rewrite/TrivialAddrOf.scala
+++ b/src/rewrite/vct/rewrite/TrivialAddrOf.scala
@@ -98,7 +98,7 @@ case class TrivialAddrOf[Pre <: Generation]() extends Rewriter[Pre] {
     val newPointer = Eval(
       PreAssignExpression(
         newTarget,
-        NewPointerArray(newValue.t, const[Post](1))(PanicBlame("Size is > 0")),
+        NewPointerArray(newValue.t, const[Post](1), None)(PanicBlame("Size is > 0")),
       )(blame)
     )
     (newPointer, newTarget, newValue)
diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala
new file mode 100644
index 0000000000..6ce0ed43f0
--- /dev/null
+++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala
@@ -0,0 +1,97 @@
+package vct.rewrite
+
+import vct.col.ast.`type`.typeclass.TFloats
+import vct.col.ast._
+import vct.col.origin.Origin
+import vct.col.rewrite.{Generation, RewriterBuilder}
+import vct.col.typerules.CoercingRewriter
+import vct.result.VerificationError.UserError
+
+case class DisallowedConstAssignment(target: Node[_]) extends UserError {
+  override def code: String = "disallowedConstAssignment"
+  override def text: String =
+    target.o.messageInContext("Cannot assign to constant target.")
+}
+
+case class DisallowedQualifiedType(target: Node[_]) extends UserError {
+  override def code: String = "disallowedQualifiedType"
+  override def text: String =
+    target.o.messageInContext("This qualified type is not allowed.")
+}
+
+case object TypeQualifierCoercion extends RewriterBuilder {
+  override def key: String = "TypeQualifierCoercion"
+  override def desc: String =
+    "Removes qualifiers from types."
+}
+
+case class TypeQualifierCoercion[Pre <: Generation]()
+    extends CoercingRewriter[Pre] {
+
+  override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(
+    implicit o: Origin
+  ): Expr[Post] = {
+    coercion match {
+      case CoerceFromConst(_) =>
+      case CoerceToConst(_) =>
+      case CoerceToUnique(_, _) =>
+      case CoerceFromUnique(_, _) =>
+      case CoerceBetweenUnique(_, _, _) =>
+      case _ =>
+    }
+    super.applyCoercion(e, coercion)
+  }
+
+  case class InnerInfo(){
+    var unique: Option[BigInt] = None
+    var const: Boolean = false
+  }
+
+  def getUnqualified(t: Type[Pre], info: InnerInfo = InnerInfo()): (InnerInfo, Type[Post]) = t match {
+    case TConst(_) | TUnique(_, _) if info.const || info.unique.isDefined =>
+      throw DisallowedQualifiedType(t)
+    case TConst(it) =>
+      info.const = true
+      getUnqualified(it, info)
+    case TUnique(it, id) =>
+      info.unique = Some(id)
+      getUnqualified(it, info)
+    case _ => (info, dispatch(t))
+  }
+
+  def makePointer(t: Type[Pre]): Type[Post] = {
+    implicit val o: Origin = t.o
+    val (info, resType) = getUnqualified(t)
+    if(info.const) TConstPointer(resType)
+    else if (info.unique.isDefined) TUniquePointer(resType, info.unique.get)
+    else TPointer(resType)
+  }
+
+  override def postCoerce(t: Type[Pre]): Type[Post] =
+    t match {
+      case TConst(t) => dispatch(t)
+      case TUnique(_, _) => throw DisallowedQualifiedType(t)
+      case TPointer(it) => makePointer(it)
+      case other => other.rewriteDefault()
+    }
+
+  override def postCoerce(e: Expr[Pre]): Expr[Post] = {
+    implicit val o: Origin = e.o
+    e match {
+      case PreAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target)
+      case PostAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target)
+      case npa @ NewPointerArray(t, size, _) =>
+        val (info, newT) = getUnqualified(t)
+        if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame)
+        else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame)
+      case other => other.rewriteDefault()
+    }
+  }
+
+  override def postCoerce(s: Statement[Pre]): Statement[Post] =
+    s match {
+      case Assign(target, _) if getUnqualified(target.t)._1.const => throw DisallowedConstAssignment(target)
+      case a@AssignInitial(target, value) => Assign(dispatch(target), dispatch(value))(a.blame)(a.o)
+      case other => other.rewriteDefault()
+    }
+}
diff --git a/src/rewrite/vct/rewrite/adt/ImportADT.scala b/src/rewrite/vct/rewrite/adt/ImportADT.scala
index 444e9eae6c..9086e62ce4 100644
--- a/src/rewrite/vct/rewrite/adt/ImportADT.scala
+++ b/src/rewrite/vct/rewrite/adt/ImportADT.scala
@@ -38,6 +38,8 @@ case object ImportADT {
       case TRef() => "ref"
       case TArray(element) => "arr_" + typeText(element)
       case TPointer(element) => "ptr_" + typeText(element)
+      case TUniquePointer(element, unique) => "unique_ptr_" + unique.toString + "_" + typeText(element)
+      case TConstPointer(element) => "const_ptr_" + typeText(element)
       case TProcess() => "proc"
       case TModel(Ref(model)) => model.o.getPreferredNameOrElse().camel
       case TAxiomatic(Ref(adt), args) =>
diff --git a/src/rewrite/vct/rewrite/adt/ImportConstPointer.scala b/src/rewrite/vct/rewrite/adt/ImportConstPointer.scala
new file mode 100644
index 0000000000..01d08693d9
--- /dev/null
+++ b/src/rewrite/vct/rewrite/adt/ImportConstPointer.scala
@@ -0,0 +1,186 @@
+package vct.col.rewrite.adt
+
+import vct.col.ast._
+import vct.col.origin._
+import vct.col.rewrite.Generation
+import vct.col.util.AstBuildHelpers.{ExprBuildHelpers, const}
+
+
+case object ImportConstPointer extends ImportADTBuilder("const_pointer") {
+  case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_])
+      extends Blame[OptionNone] {
+    override def blame(error: OptionNone): Unit = inner.blame(PointerNull(expr))
+  }
+
+  case class PointerBoundsPreconditionFailed(
+      inner: Blame[PointerBounds],
+      expr: Node[_],
+  ) extends Blame[PreconditionFailed] {
+    override def blame(error: PreconditionFailed): Unit =
+      inner.blame(PointerBounds(expr))
+  }
+
+  case class DerefPointerBoundsPreconditionFailed(
+      inner: Blame[PointerDerefError],
+      expr: Expr[_],
+  ) extends Blame[PreconditionFailed] {
+    override def blame(error: PreconditionFailed): Unit =
+      inner.blame(PointerInsufficientPermission(expr))
+  }
+
+  case class PointerFieldInsufficientPermission(
+      inner: Blame[PointerInsufficientPermission],
+      expr: Expr[_],
+  ) extends Blame[InsufficientPermission] {
+    override def blame(error: InsufficientPermission): Unit =
+      inner.blame(PointerInsufficientPermission(expr))
+  }
+}
+
+case class ImportConstPointer[Pre <: Generation](importer: ImportADTImporter)
+    extends ImportADT[Pre](importer) {
+  import ImportConstPointer._
+
+  private lazy val pointerFile = parse("const_pointer")
+
+  private lazy val pointerAdt = find[AxiomaticDataType[Post]](
+    pointerFile,
+    "const_pointer",
+  )
+  private lazy val pointerOf = find[ADTFunction[Post]](pointerAdt, "const_pointer_of")
+  private lazy val pointerBlock = find[ADTFunction[Post]](
+    pointerAdt,
+    "const_pointer_block",
+  )
+  private lazy val pointerOffset = find[ADTFunction[Post]](
+    pointerAdt,
+    "const_pointer_offset",
+  )
+  private lazy val pointerDeref = find[Function[Post]](pointerFile, "const_ptr_deref")
+  private lazy val pointerAdd = find[Function[Post]](pointerFile, "const_ptr_add")
+
+  def isConstPointer(e: Expr[Pre]): Boolean = e.t match {
+    case TConstPointer(_) => true
+    case _ => false
+  }
+
+  def getInner(t: Type[Pre]): Type[Pre] = t match {
+    case TConstPointer(inner) => inner
+    case _ => ???
+  }
+
+  override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(
+      implicit o: Origin
+  ): Expr[Post] =
+    coercion match {
+      case CoerceNullPointer(TConstPointer(_)) => OptNone()
+      case other => super.applyCoercion(e, other)
+    }
+
+  override def postCoerce(t: Type[Pre]): Type[Post] =
+    t match {
+      case TConstPointer(inner) => TOption(TAxiomatic(pointerAdt.ref, Seq(dispatch(inner))))
+      case other => other.rewriteDefault()
+    }
+
+  override def postCoerce(location: Location[Pre]): Location[Post] =
+    location match {
+      case loc @ PointerLocation(pointer) if isConstPointer(pointer) =>
+        ??? // Should not happen?
+      case other => other.rewriteDefault()
+    }
+
+  override def postCoerce(e: Expr[Pre]): Expr[Post] = {
+    implicit val o: Origin = e.o
+    e match {
+      case sub @ PointerSubscript(pointer, index) if isConstPointer(pointer) =>
+        val inner = dispatch(getInner(pointer.t))
+        FunctionInvocation[Post](
+          ref = pointerDeref.ref,
+          args = Seq(
+            FunctionInvocation[Post](
+              ref = pointerAdd.ref,
+              args = Seq(
+                OptGet(dispatch(pointer))(
+                  PointerNullOptNone(sub.blame, pointer)
+                ),
+                dispatch(index),
+              ),
+              typeArgs = Seq(inner),
+              Nil,
+              Nil,
+            )(NoContext(PointerBoundsPreconditionFailed(sub.blame, index)))
+          ),
+          typeArgs = Seq(inner),
+          Nil,
+          Nil,
+        )(PanicBlame("ptr_deref requires nothing."))
+      case add @ PointerAdd(pointer, offset) if isConstPointer(pointer) =>
+        val inner = dispatch(getInner(pointer.t))
+        OptSome(
+          FunctionInvocation[Post](
+            ref = pointerAdd.ref,
+            args = Seq(
+              OptGet(dispatch(pointer))(PointerNullOptNone(add.blame, pointer)),
+              dispatch(offset),
+            ),
+            typeArgs = Seq(inner),
+            Nil,
+            Nil,
+          )(NoContext(PointerBoundsPreconditionFailed(add.blame, pointer)))
+        )
+      case deref @ DerefPointer(pointer) if isConstPointer(pointer) =>
+//        val c_pointer = OptGet(dispatch(pointer))(PointerNullOptNone(sub.blame, pointer))
+//        //        val blame = NoContext(PointerBoundsPreconditionFailed(sub.blame, index))
+//        SeqSubscript(c_pointer, dispatch(index))(PanicBlame("TODO: pointer subscript out of bounds"))
+        val inner = dispatch(getInner(pointer.t))
+        FunctionInvocation[Post](
+          ref = pointerDeref.ref,
+          args = Seq(
+            FunctionInvocation[Post](
+              ref = pointerAdd.ref,
+              // Always index with zero, otherwise quantifiers with pointers do not get triggered
+              args = Seq(
+                OptGet(dispatch(pointer))(
+                  PointerNullOptNone(deref.blame, pointer)
+                ),
+                const(0),
+              ),
+              typeArgs = Seq(inner),
+              Nil,
+              Nil,
+            )(NoContext(
+              DerefPointerBoundsPreconditionFailed(deref.blame, pointer)
+            ))
+          ),
+          typeArgs = Seq(inner),
+          Nil,
+          Nil,
+        )(PanicBlame("ptr_deref requires nothing."))
+      case len @ PointerBlockLength(pointer) if isConstPointer(pointer) =>
+        val inner = dispatch(getInner(pointer.t))
+        Size(ADTFunctionInvocation[Post](
+            typeArgs = Some((pointerAdt.ref, Seq(inner))),
+            ref = pointerBlock.ref,
+            args = Seq(
+              OptGet(dispatch(pointer))(PointerNullOptNone(len.blame, pointer))
+            ),
+          ))
+      case off @ PointerBlockOffset(pointer) if isConstPointer(pointer) =>
+        val inner = dispatch(getInner(pointer.t))
+        ADTFunctionInvocation[Post](
+          typeArgs = Some((pointerAdt.ref, Seq(inner))),
+          ref = pointerOffset.ref,
+          args = Seq(
+            OptGet(dispatch(pointer))(PointerNullOptNone(off.blame, pointer))
+          ),
+        )
+      case pointerLen @ PointerLength(pointer) if isConstPointer(pointer) =>
+        postCoerce(
+          PointerBlockLength(pointer)(pointerLen.blame) -
+            PointerBlockOffset(pointer)(pointerLen.blame)
+        )
+      case other => other.rewriteDefault()
+    }
+  }
+}
diff --git a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
index e66592de4b..b819092126 100644
--- a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
@@ -107,7 +107,7 @@ case object LangCPPToCol {
           kernelLambda.blame.blame(SYCLKernelLambdaFailure(
             KernelPostconditionFailed(failure, Right(kernelLambda))
           ))
-        case TerminationMeasureFailed(applicable, apply, measure) =>
+        case error: TerminationMeasureFailed =>
           PanicBlame("Kernel lambdas do not have a termination measure yet")
             .blame(error)
         case ContextEverywhereFailedInPost(failure, node) =>
@@ -510,7 +510,7 @@ case object LangCPPToCol {
             (node.o, c.descInContext + ", since ..."),
             (failure.node.o, "... " + failure.descCompletion),
           )
-        case TerminationMeasureFailed(_, _, _) =>
+        case error: TerminationMeasureFailed =>
           PanicBlame(
             "This kernel class constructor should always be able to terminate."
           ).blame(error)
@@ -2733,11 +2733,11 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         (sizeOption, init.init) match {
           case (None, None) => throw WrongCPPType(decl)
           case (Some(size), None) =>
-            val newArr = NewPointerArray[Post](t, rw.dispatch(size))(cta.blame)
+            val newArr = NewPointerArray[Post](t, rw.dispatch(size), None)(cta.blame)
             Block(Seq(LocalDecl(v), assignLocal(v.get, newArr)))
           case (None, Some(CPPLiteralArray(exprs))) =>
             val newArr =
-              NewPointerArray[Post](t, c_const[Post](exprs.size))(cta.blame)
+              NewPointerArray[Post](t, c_const[Post](exprs.size), None)(cta.blame)
             Block(
               Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
                 assignliteralArray(v, exprs, o)
@@ -2748,7 +2748,7 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
             if (realSize < exprs.size)
               logger.warn(s"Excess elements in array initializer: '${decl}'")
             val newArr =
-              NewPointerArray[Post](t, c_const[Post](realSize))(cta.blame)
+              NewPointerArray[Post](t, c_const[Post](realSize), None)(cta.blame)
             Block(
               Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
                 assignliteralArray(v, exprs.take(realSize.intValue), o)
diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala
index d2aa6bfe68..e74599d63e 100644
--- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala
@@ -391,17 +391,20 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
 
   def getBaseType[G](t: Type[G]): Type[G] =
     t match {
-      case CPrimitiveType(specs) => C.getPrimitiveType(specs)
+      case CPrimitiveType(specs) => getBaseType(C.getPrimitiveType(specs, Some(t)))
+      case TUnique(it, _) => getBaseType(it)
+      case TConst(it) => getBaseType(it)
       case _ => t
     }
 
-  def castIsId(exprType: Type[Pre], castType: Type[Pre]): Boolean =
-    (castType, getBaseType(exprType)) match {
+  def castIsId(exprType: Type[Pre], castType: Type[Pre]): Boolean = {
+    (getBaseType(castType), getBaseType(exprType)) match {
       case (tc, te) if tc == te => true
       case (TCInt(), TBoundedInt(_, _)) => true
       case (TBoundedInt(_, _), TCInt()) => true
       case _ => false
     }
+  }
 
   def cast(c: CCast[Pre]): Expr[Post] =
     c match {
@@ -413,8 +416,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         CastFloat[Post](rw.dispatch(c.expr), rw.dispatch(t))(c.o)
       case CCast(
             inv @ CInvocation(CLocal("__vercors_malloc"), Seq(arg), Nil, Nil),
-            CTPointer(t2),
+            tcast,
           ) =>
+        val t2 = tcast match {
+          case CTPointer(t2) => t2
+          case _ => throw UnsupportedMalloc(c)
+        }
         val (t1, size) =
           arg match {
             case SizeOf(t1) if castIsId(t1, t2) => (t1, c_const[Post](1)(c.o))
@@ -424,7 +431,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
               (t1, rw.dispatch(r))
             case _ => throw UnsupportedMalloc(c)
           }
-        NewPointerArray(rw.dispatch(t1), size)(ArrayMallocFailed(inv))(c.o)
+        NewPointerArray(rw.dispatch(t2), size, None)(ArrayMallocFailed(inv))(c.o)
       case CCast(CInvocation(CLocal("__vercors_malloc"), _, _, _), _) =>
         throw UnsupportedMalloc(c)
       case CCast(n @ Null(), t) if t.asPointer.isDefined => rw.dispatch(n)
@@ -482,9 +489,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     }
     val prop = new TypeProperties(cParam.specifiers, cParam)
     if(!prop.validCParam) throw WrongCType(cParam)
-    val specType = if(prop.unique.isEmpty)
-      rw.dispatch(prop.mainType.get) else
-      TUniquePointer(rw.dispatch(prop.innerType.get), prop.unique.get)(cParam.o)
+    val specType = rw.dispatch(prop.mainType.get)
 
     cParam.drop()
     val v =
@@ -630,7 +635,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     t match {
       case TArray(element) => element
       case TPointer(element) => element
-      case TUniquePointer(element, _) => element
       case _ => throw Unreachable("Already checked on pointer or array type")
     }
 
@@ -646,12 +650,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         val v = new Variable[Post](TCInt())(varO)
         dynamicSharedMemLengthVar(d) = v
         rw.variables.declare(v)
-//      val decl: Statement[Post] = LocalDecl(cNameSuccessor(d))
         val assign: Statement[Post] = assignLocal(
           Local(cNameSuccessor(d).ref),
           NewPointerArray[Post](
             getInnerType(cNameSuccessor(d).t),
-            Local(v.ref),
+            Local(v.ref), None
           )(PanicBlame("Shared memory sizes cannot be negative.")),
         )
         declarations ++= Seq(cNameSuccessor(d))
@@ -659,13 +662,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
       })
       staticSharedMemNames.foreach { case (d, (size, blame)) =>
         implicit val o: Origin = getCDecl(d).o
-//      val decl: Statement[Post] = LocalDecl(cNameSuccessor(d))
         val assign: Statement[Post] = assignLocal(
           Local(cNameSuccessor(d).ref),
           // Since we set the size and blame together, we can assume the blame is not None
           NewPointerArray[Post](
             getInnerType(cNameSuccessor(d).t),
-            CIntegerValue(size),
+            CIntegerValue(size), None
           )(blame.get),
         )
         declarations ++= Seq(cNameSuccessor(d))
@@ -866,29 +868,21 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     var sizeBlame: Option[Blame[ArraySizeError]] = None
     var pure = false
     var inline = false
-    var unique: Option[BigInt] = None
     var static = false
 
     specs.foreach {
       case GPULocal() => shared = true
       case GPUGlobal() => global = true
-      case CSpecificationType(t@CTPointer(it)) =>
+      case CSpecificationType(t) if isPointer(t) =>
+        val (inner, size, blame) = getInnerPointerInfo(t).get
         arrayOrPointer = true
-        innerType = Some(it)
+        innerType = Some(inner)
         mainType = Some(t)
-      case CSpecificationType(t @ CTArray(size, it)) =>
+        sizeBlame = blame
         arraySize = size
-        innerType = Some(it)
-        sizeBlame = Some(
-          t.blame
-        ) // we set the blame here, together with the size
-        arrayOrPointer = true
-        mainType = Some(t)
       case CSpecificationType(t) =>
         mainType = Some(t)
       case CExtern() => extern = true
-      case CUnique(i) if unique.isDefined => throw WrongCType(decl)
-      case CUnique(i) => unique = Some(i)
       case CPure() => pure = true
       case CInline() => inline = true
       case CStatic() => static = true
@@ -898,8 +892,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
 
     def isShared: Boolean = shared && !global
     def isGlobal: Boolean = !shared && global
-    def validNonGpu: Boolean = !global && !shared &&
-      (unique.isEmpty || (unique.isDefined && arrayOrPointer)) && mainType.isDefined
+    def validNonGpu: Boolean = !global && !shared && mainType.isDefined
     def validReturn: Boolean = validNonGpu && !static
     def validCParam: Boolean = !pure && !inline && validNonGpu && !static
     def validCLocal = validCParam
@@ -1092,12 +1085,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
   ): Seq[Statement[Post]] = {
     implicit val o: Origin = origin
     (exprs.zipWithIndex.map { case (value, index) =>
-      Assign[Post](
+      // Since we model const arrays with sequences internally, we cannot assign to them, so we assume their values
+        Assume[Post](
         AmbiguousSubscript(array.get, c_const(index))(PanicBlame(
-          "The explicit initialization of an array in C should never generate an assignment that exceeds the bounds of the array"
-        )),
-        rw.dispatch(value),
-      )(PanicBlame("Assignment for an explicit array initializer cannot fail."))
+          "The explicit initialization of an array in C should never exceed the bounds of the array"
+        )) === rw.dispatch(value),
+        )
     })
   }
 
@@ -1116,7 +1109,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
       case CLiteralArray(exprs) if exprs.size == size =>
         Block(Seq(
           LocalDecl(v),
-          assignLocal(
+          assignInitial(
             v.get,
             LiteralVector[Post](
               rw.dispatch(t.innerType),
@@ -1131,43 +1124,40 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
   def rewriteArrayDeclaration(
       decl: CLocalDeclaration[Pre],
       cta: CTArray[Pre],
+      init: CInit[Pre]
   ): Statement[Post] = {
-    // LangTypesToCol makes it so that each declaration only has one init
-    val init = decl.decl.inits.head
+    implicit val o: Origin = decl.o
     val info = C.getDeclaratorInfo(init.decl)
-    implicit val o: Origin = init.o
+    val CTArray(sizeOption, oldT) = cta
+    val it = rw.dispatch(oldT)
+    val t = TPointer[Post](it)
+    val v = new Variable[Post](t)(o.sourceName(info.name))
+    cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v
+    val newArrf = (size: Expr[Post]) => {
+      NewPointerArray[Post](it, size, None)(cta.blame)
+    }
 
-    decl.decl.specs match {
-      case Seq(CSpecificationType(cta @ CTArray(sizeOption, oldT))) =>
-        val t = rw.dispatch(oldT)
-        val v = new Variable[Post](TPointer(t))(o.sourceName(info.name))
-        cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v
-
-        (sizeOption, init.init) match {
-          case (None, None) => throw WrongCType(decl)
-          case (Some(size), None) =>
-            val newArr = NewPointerArray[Post](t, rw.dispatch(size))(cta.blame)
-            Block(Seq(LocalDecl(v), assignLocal(v.get, newArr)))
-          case (None, Some(CLiteralArray(exprs))) =>
-            val newArr =
-              NewPointerArray[Post](t, c_const[Post](exprs.size))(cta.blame)
-            Block(
-              Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
-                assignliteralArray(v, exprs, o)
-            )
-          case (Some(size), Some(CLiteralArray(exprs))) =>
-            val realSize = isConstantInt(size).filter(_ >= 0)
-              .getOrElse(throw WrongCType(decl))
-            if (realSize < exprs.size)
-              logger.warn(s"Excess elements in array initializer: '${decl}'")
-            val newArr =
-              NewPointerArray[Post](t, c_const[Post](realSize))(cta.blame)
-            Block(
-              Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
-                assignliteralArray(v, exprs.take(realSize.intValue), o)
-            )
-          case _ => throw WrongCType(decl)
-        }
+    (sizeOption, init.init) match {
+      case (None, None) => throw WrongCType(decl)
+      case (Some(size), None) =>
+        val newArr = newArrf(rw.dispatch(size))
+        Block(Seq(LocalDecl(v), assignInitial(v.get, newArr)))
+      case (None, Some(CLiteralArray(exprs))) =>
+        val newArr = newArrf(c_const[Post](exprs.size))
+        Block(
+          Seq(LocalDecl(v), assignInitial(v.get, newArr)) ++
+            assignliteralArray(v, exprs, o)
+        )
+      case (Some(size), Some(CLiteralArray(exprs))) =>
+        val realSize = isConstantInt(size).filter(_ >= 0)
+          .getOrElse(throw WrongCType(decl))
+        if (realSize < exprs.size)
+          logger.warn(s"Excess elements in array initializer: '${decl}'")
+        val newArr = newArrf(c_const[Post](realSize))
+        Block(
+          Seq(LocalDecl(v), assignInitial(v.get, newArr)) ++
+            assignliteralArray(v, exprs.take(realSize.intValue), o)
+        )
       case _ => throw WrongCType(decl)
     }
   }
@@ -1196,27 +1186,23 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
       )
     ).getOrElse(NewObject[Post](targetClass.ref))
 
-    Block(Seq(LocalDecl(v), assignLocal(v.get, initialVal)))
+    Block(Seq(LocalDecl(v), assignInitial(v.get, initialVal)))
   }
 
   def rewriteLocal(decl: CLocalDeclaration[Pre]): Statement[Post] = {
     decl.drop()
-    decl.decl.specs.foreach {
-      case _: CSpecificationType[Pre] =>
-      case _ => throw WrongCType(decl)
-    }
-
+    val prop = new TypeProperties(decl.decl.specs, decl)
+    if(!prop.validCLocal) throw WrongCType(decl)
     // LangTypesToCol makes it so that each declaration only has one init
     val init = decl.decl.inits.head
 
-    val t =
-      decl.decl.specs.collectFirst { case t: CSpecificationType[Pre] => t.t }
-        .get match {
+    val t = prop.mainType.get match {
         case t: CTVector[Pre] if init.init.collect({
               case _: CLiteralArray[Pre] => true
             }).isDefined =>
           return rewriteVectorDeclaration(decl, t, init)
-        case t: CTArray[Pre] => return rewriteArrayDeclaration(decl, t)
+        case t: CTArray[Pre] =>
+          return rewriteArrayDeclaration(decl, t, init)
         case t: CTStruct[Pre] => return rewriteStructDeclaration(decl, t)
         case t => rw.dispatch(t)
       }
@@ -1226,7 +1212,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v
     implicit val o: Origin = init.o
     init.init.map(value =>
-      Block(Seq(LocalDecl(v), assignLocal(v.get, rw.dispatch(value))))
+      Block(Seq(LocalDecl(v), assignInitial(v.get, rw.dispatch(value))))
     ).getOrElse(LocalDecl(v))
   }
 
@@ -1266,16 +1252,39 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     )(KernelBarrierFailure(barrier))
   }
 
-  def isPointer(t: Type[Pre]): Boolean = getPointer(t).isDefined
-
-  def getPointer(t: Type[Pre]): Option[Type[Pre]] =
+  def getInnerPointerInfo(t: Type[Pre]) : Option[(Type[Pre], Option[Expr[Pre]], Option[Blame[ArraySizeError]])] =
     getBaseType(t) match {
-      case t @ TPointer(_) => Some(t)
-      case t @ TUniquePointer(_, _) => Some(t)
-      case t @ CTPointer(_) => Some(t)
+      case TPointer(it) => Some((it, None, None))
+      case CTPointer(it) => Some((it, None, None))
+      case a@CTArray(size, it) => Some((it, size, Some(a.blame)))
       case _ => None
     }
 
+  def isVector(t: Type[Pre]): Boolean =
+    getBaseType(t) match {
+      case t : CTVector[Pre] => true
+      case _ => false
+    }
+
+  def isArray(t: Type[Pre]): Boolean =
+    getBaseType(t) match {
+      case t : CTArray[Pre] => true
+      case _ => false
+    }
+
+  def isStruct(t: Type[Pre]): Boolean =
+    getBaseType(t) match {
+      case t : CTStruct[Pre] => true
+      case _ => false
+    }
+
+  def isPointer(t: Type[Pre]): Boolean =
+    getBaseType(t) match {
+      case t @ TPointer(_) => true
+      case t @ CTPointer(_) => true
+      case _ => false
+    }
+
   def isNumeric(t: Type[Pre]): Boolean =
     getBaseType(t) match {
       case _: NumericType[Pre] => true
@@ -1510,8 +1519,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         Seq(
           LocalDecl(vCopy),
           LocalDecl(vValue),
-          assignLocal(vValue.get, value),
-          assignLocal(vCopy.get, NewObject[Post](targetClass.ref)),
+          assignInitial(vValue.get, value),
+          assignInitial(vCopy.get, NewObject[Post](targetClass.ref)),
         ) ++ fieldAssigns
       ),
       vCopy.get,
@@ -1655,7 +1664,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     val before: Statement[Post] =
       Block[Post](Seq(
         LocalDecl(rhs_val)(rhs.o),
-        assignLocal(rhs_val.get(rhs.o), rhs)(rhs.o),
+        assignInitial(rhs_val.get(rhs.o), rhs)(rhs.o),
       ))(assign.o)
 
     // Assign the correct values
@@ -1685,12 +1694,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     )(assign.o)
   }
 
-  def isCPointer(t: Type[_]) =
-    getBaseType(t) match {
-      case CTPointer(_) => true
-      case _ => false
-    }
-
   def indexVectors(
       e: Expr[Post],
       askedType: Type[Post],
@@ -1728,7 +1731,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
               val v = new Variable[Post](e.t)
               val befores: Seq[Statement[Post]] = Seq(
                 LocalDecl(v),
-                assignLocal(v.get, e),
+                assignInitial(v.get, e),
               )
               (befores, v.get)
           }
@@ -1957,7 +1960,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
 
     (e.name, args, givenMap, yields) match {
       case (_, _, g, y) if g.nonEmpty || y.nonEmpty =>
-      case ("__vercors_free", Seq(xs), _, _) if isCPointer(xs.t) =>
+      case ("__vercors_free", Seq(xs), _, _) if isPointer(xs.t) =>
         return FreePointer[Post](rw.dispatch(xs))(inv.blame)(inv.o)
       case _ => ()
     }
@@ -1993,8 +1996,9 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     }
   }
 
-  def pointerType(t: CTPointer[Pre]): Type[Post] = {
-    TPointer(rw.dispatch(t.innerType))
+  def pointerType(t: CPointerType[Pre]): Type[Post] = t match {
+    case CTPointer(innerType) => TPointer(rw.dispatch(innerType))
+    case CTArray(_, innerType) => TPointer(rw.dispatch(innerType))
   }
 
   def vectorType(t: CType[Pre]): Type[Post] = {
diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
index 213997930e..5f34c6d49f 100644
--- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
@@ -393,6 +393,7 @@ case class LangSpecificToCol[Pre <: Generation](
   override def dispatch(t: Type[Pre]): Type[Post] =
     t match {
       case t: JavaTClass[Pre] => java.classType(t)
+      case t: CPointerType[Pre] => c.pointerType(t)
       case t: CTPointer[Pre] => c.pointerType(t)
       case t: CTVector[Pre] => c.vectorType(t)
       case t: TOpenCLVector[Pre] => c.vectorType(t)
diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala
index 6b7f9fe8eb..a6b6c290d0 100644
--- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala
@@ -115,12 +115,14 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] {
       implicit o: Origin
   ): (Seq[CDeclarationSpecifier[Post]], CDeclarator[Post]) = {
     val info = C.getDeclaratorInfo(declarator)
-    val baseType = C.getPrimitiveType(specifiers, context)
-    val otherSpecifiers = specifiers
-      .filter(!_.isInstanceOf[CTypeSpecifier[Pre]]).map(dispatch)
-    val newSpecifiers =
+    val (specs, otherSpecifiers) = specifiers
+      .partition({case _ : CTypeSpecifier[Pre] => true; case _: CTypeQualifierDeclarationSpecifier[Pre] => true;
+      case _ => false})
+    val newOtherSpecifiers = otherSpecifiers.map(dispatch)
+    val baseType = C.getPrimitiveType(specs, context)
+    val newSpecifiers : Seq[CDeclarationSpecifier[LangTypesToCol.this.Post]] =
       CSpecificationType[Post](dispatch(info.typeOrReturnType(baseType))) +:
-        otherSpecifiers
+        newOtherSpecifiers
     val newDeclarator =
       info.params match {
         case Some(params) =>
diff --git a/src/viper/viper/api/backend/SilverBackend.scala b/src/viper/viper/api/backend/SilverBackend.scala
index 2e1161e85e..31d757d5dc 100644
--- a/src/viper/viper/api/backend/SilverBackend.scala
+++ b/src/viper/viper/api/backend/SilverBackend.scala
@@ -285,18 +285,10 @@ trait SilverBackend
           case PredicateNotWellformed(_, reason, _) => defer(reason)
           case FunctionTerminationError(node: Infoed, reason, _) =>
             val apply = get[col.Invocation[_]](node)
-            apply.ref.decl.blame.blame(blame.TerminationMeasureFailed(
-              apply.ref.decl,
-              apply,
-              getDecreasesClause(reason),
-            ))
+            apply.ref.decl.blame.blame(getDecreasesBlame(apply, reason))
           case MethodTerminationError(node: Infoed, reason, _) =>
-            val apply = get[col.Invocation[_]](node)
-            apply.ref.decl.blame.blame(blame.TerminationMeasureFailed(
-              apply.ref.decl,
-              apply,
-              getDecreasesClause(reason),
-            ))
+            val apply = get[col.InvokingNode[_]](node)
+            apply.ref.decl.blame.blame(getDecreasesBlame(apply, reason))
           case LoopTerminationError(node: Infoed, reason, _) =>
             val decreases = get[col.DecreasesClause[_]](node)
             info(node).invariant.get.blame
@@ -395,6 +387,19 @@ trait SilverBackend
       case _ => ???
     }
 
+  def getDecreasesBlame(invoking: col.InvokingNode[_], reason: ErrorReason) : blame.TerminationMeasureFailed = {
+    reason match {
+      case TerminationConditionFalse(node: Infoed) =>
+        val procedure = get[col.Procedure[_]](node)
+        blame.CallTerminationMeasureFailed(invoking, procedure)
+      case _ => blame.DecreaseTerminationMeasureFailed(
+        invoking.ref.decl,
+        invoking,
+        getDecreasesClause(reason),
+      )
+    }
+  }
+
   def getDecreasesClause(reason: ErrorReason): col.DecreasesClause[_] =
     reason match {
       case TerminationConditionFalse(node) =>
diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala
new file mode 100644
index 0000000000..8744be633f
--- /dev/null
+++ b/test/main/vct/test/integration/examples/QualifierSpec.scala
@@ -0,0 +1,52 @@
+package vct.test.integration.examples
+
+import vct.test.integration.helper.VercorsSpec
+
+class QualifierSpec extends VercorsSpec {
+  vercors should verify using silicon example "concepts/unique/arrays.c"
+
+  vercors should verify using silicon in "same uniques pointer parameter" c """void f(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){x1 = x0;}"""
+  vercors should verify using silicon in "same uniques array parameter" c """void f(/*@ unique<1> @*/ int x0[], /*@ unique<1> @*/ int x1[]){x1 = x0;}"""
+  vercors should verify using silicon in "same uniques local" c """void f(){/*@ unique<1> @*/ int x0[2]; /*@ unique<1> @*/ int* x1; x1 = x0;}"""
+  vercors should verify using silicon in "same uniques local with inits" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<1> @*/ int* x1; x1 = x0;}"""
+  vercors should verify using silicon in "malloc uniques" c
+    """#include <stdlib.h>
+  void f(){/*@ unique<1> @*/ int* x0 = (/*@ unique<1> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0;}"""
+  vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}"""
+
+  vercors should error withCode "resolutionError:type" in "malloc different uniques" c
+    """#include <stdlib.h>
+  void f(){/*@ unique<1> @*/ int* x0; x0 = (/*@ unique<2> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0;}"""
+
+  vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 1" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<3> @*/ int * /*@ unique<4> @*/ * x1; x0 = x1;}"""
+  vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 2" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<1> @*/ int * /*@ unique<4> @*/ * x1; x0 = x1;}"""
+  vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 3" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<3> @*/ int * /*@ unique<2> @*/ * x1; x0 = x1;}"""
+
+  vercors should error withCode "cTypeNotSupported" in "multiple uniques" c """void f(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}"""
+  vercors should error withCode "resolutionError:type" in "different uniques param - 1" c """void f(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}"""
+  vercors should error withCode "resolutionError:type" in "different uniques param - 2" c """void f(/*@ unique<1> @*/ int* x0){ /*@ unique<2> @*/ int* x1 = x0;}"""
+  vercors should error withCode "resolutionError:type" in "different uniques local" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<2> @*/ int* x1; x1 = x0;}"""
+  vercors should error withCode "resolutionError:type" in "multiple uniques parameter" c """void f(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}"""
+
+  vercors should verify using silicon in "Assign to init const" c """void f(){const int x = 2; /*@ assert x == 2; @*/}"""
+  vercors should error withCode "disallowedConstAssignment" in "Assign to local const" c """void f(){const int x; x = 0;}"""
+  vercors should error withCode "disallowedConstAssignment" in "Assign to param const" c """void f(const int x){x = 0;}"""
+
+  vercors should verify using silicon in "Assign to init const array" c """void f(){const int x[2] = {0, 2}; /*@ assert x[1] == 2; @*/}"""
+  vercors should error withCode "disallowedConstAssignment" in "Assign to local array of consts" c """void f(){const int x[2] = {0, 2}; x[0] = 1;}"""
+  vercors should error withCode "disallowedConstAssignment" in "Assign to local pointer of consts" c """void f(){const int *x; x[0] = 1;}"""
+  vercors should error withCode "disallowedConstAssignment" in "Assign to param pointer of consts" c """void f(const int *x){x[0] = 1;}"""
+
+  vercors should verify using silicon in "Assign const array to const pointer" c """void f(const int* y){const int x[2] = {0, 2}; y = x;}"""
+  vercors should error withCode "resolutionError:type" in "Assign const array to non-const pointer" c """void f(int* y){const int x[2] = {0, 2}; x = y;}"""
+
+  vercors should error withCode "disallowedConstAssignment" in "Assign const pointer" c """void f(int* const y){int* const x; y = x;}"""
+  vercors should verify using silicon in "Assign element of const pointer" c
+    """/*@ context x!=NULL ** \pointer_length(x) == 1 ** Perm(&x[0], write); ensures x[0] == 1;@*/
+  void f(int * const x){x[0] = 1;}"""
+}
+
+class QualifierSpecWIP extends VercorsSpec {
+  vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}"""
+
+}
\ No newline at end of file
diff --git a/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala b/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala
deleted file mode 100644
index 8fc4d821d0..0000000000
--- a/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-package vct.test.integration.examples
-
-import vct.test.integration.helper.VercorsSpec
-
-class UniqueFieldsSpec extends VercorsSpec {
-  vercors should verify using silicon example "concepts/unique/arrays.c"
-
-  vercors should error withCode "wrongCType" in "multiple uniques" c """int main(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}"""
-  vercors should error withCode "resolutionError:type" in "different uniques local" c """int main(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}"""
-  vercors should error withCode "resolutionError:type" in "multiple uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}"""
-  vercors should verify using silicon in "same uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){x1 = x0;}"""
-}