diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala
index 39cdc67ab2..f0b4c3438f 100644
--- a/src/parsers/vct/parsers/transform/PVLToCol.scala
+++ b/src/parsers/vct/parsers/transform/PVLToCol.scala
@@ -387,8 +387,8 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val
 
   def convert(implicit subject: SubjectContext): PVLCommunicateSubject[G] = subject match {
     case Subject0(name) => PVLThreadName(convert(name))
-    case Subject1(family, _, expr, _) => PVLIndexedFamilyName(convert(family), convert(expr))
-    case Subject2(family, _, binder, _, start, _, end, _) => PVLFamilyRange(convert(family), convert(binder), convert(start), convert(end))
+    case Subject1(family, _, expr, _) => ??(subject)
+    case Subject2(family, _, binder, _, start, _, end, _) => ??(subject)
   }
 
   def convert(implicit region: ParRegionContext): ParRegion[G] = region match {
diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala
index 64a8dc82c1..66dc182481 100644
--- a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala
@@ -10,11 +10,13 @@ import vct.col.rewrite.lang.LangSpecificToCol.{NotAValue, ThisVar}
 import vct.col.ref.Ref
 import vct.col.resolve.ctx.{BuiltinField, BuiltinInstanceMethod, ImplicitDefaultPVLConstructor, PVLBuiltinInstanceMethod, RefADTFunction, RefAxiomaticDataType, RefClass, RefEnum, RefEnumConstant, RefField, RefFunction, RefInstanceFunction, RefInstanceMethod, RefInstancePredicate, RefModel, RefModelAction, RefModelField, RefModelProcess, RefPVLConstructor, RefPredicate, RefProcedure, RefProverFunction, RefVariable, RefVeyMontThread}
 import vct.col.util.{AstBuildHelpers, SuccessionMap}
-import vct.result.VerificationError.SystemError
+import vct.result.VerificationError.{SystemError, UserError}
+import LangPVLToCol.CommunicateNotSupported
 
 case object LangPVLToCol {
-  case object CommunicateNotSupported extends SystemError {
+  case object CommunicateNotSupported extends UserError {
     override def text: String = "The `communicate` statement is not yet supported"
+    override def code: String = "communicateNotSupported"
   }
 }
 
@@ -166,6 +168,6 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   }
 
   def communicate(comm: PVLCommunicate[Pre]): VeyMontCommExpression[Post] = {
-    throw LangPVLToCol.CommunicateNotSupported
+    throw CommunicateNotSupported
   }
 }
diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
index 0b1afe0cd8..960d77642b 100644
--- a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
+++ b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
@@ -3,7 +3,7 @@ package vct.test.integration.examples
 import vct.test.integration.helper.VercorsSpec
 
 class TechnicalVeymontSpec extends VercorsSpec {
-  vercors should verify using silicon in "example using communicate" pvl
+  vercors should error withCode "communicateNotSupported" in "example using communicate" pvl
   """
      class Storage {
         int x;
@@ -20,7 +20,7 @@ class TechnicalVeymontSpec extends VercorsSpec {
      }
   """
 
-  vercors should verify using silicon in "parameterized sends not yet supported " pvl
+  vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl
   """
     seq_program Example() {
       thread alice[10] = Storage();