diff --git a/.build/k b/.build/k
index 748a6d579..bb0ebdce5 160000
--- a/.build/k
+++ b/.build/k
@@ -1 +1 @@
-Subproject commit 748a6d57943317c0470eb8a136c205fd4da3029f
+Subproject commit bb0ebdce5a1f94dfc86baaa5f75b97f8c8248b67
diff --git a/Dockerfile b/Dockerfile
index 7d9cb9584..f60fe2d0e 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -4,12 +4,25 @@ FROM runtimeverificationinc/kframework:ubuntu-bionic
 # Install packages. #
 #####################
 
-RUN     apt-get update -q \
-    &&  apt install --yes \
-          libstdc++6      \
-          llvm-6.0        \
-          clang++-6.0     \
-          clang-6.0
+RUN   apt-get update -q     \
+  &&  apt-get install --yes \
+        libstdc++6          \
+        llvm-6.0            \
+        clang++-6.0         \
+        clang-6.0           \
+        clang-8             \
+        libclang-8-dev      \
+        llvm-8-tools        \
+        lld-8               \
+        zlib1g-dev          \
+        bison               \
+        flex                \
+        libboost-test-dev   \
+        libgmp-dev          \
+        libmpfr-dev         \
+        libyaml-dev         \
+        libjemalloc-dev     \
+        pkg-config
 
 RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.7 \
     && cd z3                                                        \
@@ -41,20 +54,21 @@ COPY --from=runtimeverificationinc/ocaml:ubuntu-bionic \
      /home/user/.opam \
      /home/user/.opam
 
-
-# This is where the rest of the dependencies go.
-ENV DEPS_DIR="/home/user/c-semantics-deps"
-
 ############
 # Build K. #
 ############
 
+# This is where the rest of the dependencies go.
+ENV DEPS_DIR="/home/user/c-semantics-deps"
+ENV PATH="${DEPS_DIR}/k/llvm-backend/src/main/native/llvm-backend/build/bin:${PATH}"
+ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin"
+
 COPY --chown=user:user ./.build/k/ ${DEPS_DIR}/k
 
 RUN cd ${DEPS_DIR}/k \
-  && mvn package -q -U \
+  && mvn package -e -q -U \
       -DskipTests -DskipKTest \
-      -Dhaskell.backend.skip -Dllvm.backend.skip \
-      -Dcheckstyle.skip
+      -Dhaskell.backend.skip \
+      -Dcheckstyle.skip \
+      -Dproject.build.type=FastBuild
 
-ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin"
diff --git a/Jenkinsfile b/Jenkinsfile
index 97d6576d9..4aa386f85 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -34,13 +34,10 @@ pipeline {
                 eval $(opam config env)
                 eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib)
                 export KOMPILE_FLAGS=-O2
-                make -j4 profile-rule-parsing --output-sync=line
+                make -j4 --output-sync=line
               '''
             } }
           }
-          post { success {
-            archiveArtifacts 'dist/timelogs.d/timelogs.csv'
-          } }
         }
         stage ( 'Re-compile w/ timeout' ) { steps {
           timeout(time: 8, unit: 'SECONDS' ) {
diff --git a/Makefile b/Makefile
index 9b28f6b69..38a808f41 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@ export KOMPILE := $(K_BIN)/kompile
 export KDEP := $(K_BIN)/kdep
 
 # Appending to whatever the environment provided.
-K_OPTS += -Xmx8g
+K_OPTS += -Xmx16g
 K_OPTS += -Xss32m
 export K_OPTS
 
diff --git a/clang-tools/ClangKast/ClangKast.cc b/clang-tools/ClangKast/ClangKast.cc
index bed0c41aa..7fdb4aac3 100644
--- a/clang-tools/ClangKast/ClangKast.cc
+++ b/clang-tools/ClangKast/ClangKast.cc
@@ -91,6 +91,7 @@ std::ostream& operator<<(std::ostream & os, const Sort & sort) {
     case Sort::NAMESPACE:             os << "Namespeace"; break;
     case Sort::NNS:                   os << "NNS"; break;
     case Sort::NNSSPECIFIER:          os << "NNSSpecifier"; break;
+    case Sort::NOINIT:                os << "NoInit"; break;
     case Sort::NONAME:                os << "NoName"; break;
     case Sort::OPID:                  os << "OpId"; break;
     case Sort::QUALIFIER:             os << "Qualifier"; break;
@@ -140,7 +141,7 @@ string Kast::Node::escapeKLabel(const string & label) {
       case '#':  subst = "Hash'"; break;
       case '$':  subst = "Dolr'"; break;
       case '%':  subst = "Perc'"; break;
-      case '&':  subst = "And'" ; break;
+      case '&':  subst = "And-'"; break;
       case '\'': subst = "Apos'"; break;
       case '(':  subst = "LPar'"; break;
       case ')':  subst = "RPar'"; break;
@@ -223,7 +224,7 @@ void Kast::KApply::print(Sort parentSort, function<void (Sort)> printChild) cons
 // *** Kast::KToken ***
 
 string Kast::KToken::toKString(const string & s) {
-  return string(Kore ? escape(s) : "\"" + escape(s) + "\"");
+  return string(Kore ? s : "\"" + escape(s) + "\"");
 }
 
 string Kast::KToken::toKString(bool b) {
@@ -330,7 +331,7 @@ void Kast::add(const T & node) {
   Kast::Nodes.push_back(make_unique<T>(node));
 }
 
-void Kast::print() { print(Sort::K, 0); }
+void Kast::print() { print(Sort::KITEM, 0); }
 
 int Kast::print(Sort parentSort, int idx) {
   if (!Nodes[idx]) throw logic_error("parse error");
diff --git a/clang-tools/ClangKast/ClangKast.h b/clang-tools/ClangKast/ClangKast.h
index ec07aa03d..91368ec09 100644
--- a/clang-tools/ClangKast/ClangKast.h
+++ b/clang-tools/ClangKast/ClangKast.h
@@ -39,6 +39,7 @@ enum class Sort {
   NAMESPACE,
   NNS,
   NNSSPECIFIER,
+  NOINIT,
   NONAME,
   OPID,
   QUALIFIER,
diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h
index 0362d1168..80222a068 100644
--- a/clang-tools/ClangKast/GetKastVisitor.h
+++ b/clang-tools/ClangKast/GetKastVisitor.h
@@ -224,22 +224,21 @@ class GetKastVisitor
       Kast::add(Kast::KApply("NestedName", Sort::NNS, {Sort::NNS, Sort::NNSSPECIFIER}));
       TRY_TO(TraverseNestedNameSpecifier(NNS->getPrefix()));
     }
-    auto nns = Kast::KApply("NNS", Sort::NNSSPECIFIER, {Sort::CID});
     switch (NNS->getKind()) {
       case NestedNameSpecifier::Identifier:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSCId", Sort::NNSSPECIFIER, {Sort::CID}));
         TRY_TO(TraverseIdentifierInfo(NNS->getAsIdentifier()));
         break;
       case NestedNameSpecifier::Namespace:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME}));
         TRY_TO(TraverseDeclarationName(NNS->getAsNamespace()->getDeclName()));
         break;
       case NestedNameSpecifier::NamespaceAlias:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME}));
         TRY_TO(TraverseDeclarationName(NNS->getAsNamespaceAlias()->getDeclName()));
         break;
       case NestedNameSpecifier::TypeSpec:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME}));
         TRY_TO(TraverseType(QualType(NNS->getAsType(), 0)));
         break;
       case NestedNameSpecifier::TypeSpecWithTemplate:
@@ -266,7 +265,7 @@ class GetKastVisitor
   bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) {
     if (!info) {
       if (decl == 0) {
-        Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME));
+        Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME));
       } else {
         Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING}));
         VisitUnsigned((unsigned long long)decl);
@@ -456,7 +455,7 @@ class GetKastVisitor
 
     if (D->isThisDeclarationADefinition()) {
       if (CXXConstructorDecl *Ctor = dyn_cast<CXXConstructorDecl>(D)) {
-        Kast::add(Kast::KApply("Constructor", Sort::STMT, {Sort::LIST, Sort::STMT}));
+        Kast::add(Kast::KApply("Constructor", Sort::STMT, {Sort::LIST, Sort::ASTMT}));
         int i = 0;
         for (auto *I : Ctor->inits()) {
           if (I->isWritten()) i++;
@@ -498,6 +497,10 @@ class GetKastVisitor
     return TraverseFunctionHelper(D);
   }
 
+  void NoInit() {
+      Kast::add(Kast::KApply("NoInit", Sort::NOINIT));
+  }
+
   bool TraverseVarHelper(VarDecl *D) {
     StorageClass(D->getStorageClass());
     ThreadStorageClass(D->getTSCSpec());
@@ -518,7 +521,7 @@ class GetKastVisitor
     if (D->getInit()) {
       TRY_TO(TraverseStmt(D->getInit()));
     } else {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     VisitBool(D->isDirectInit());
     return true;
@@ -545,7 +548,7 @@ class GetKastVisitor
     } else if (D->hasInClassInitializer()) {
       TRY_TO(TraverseStmt(D->getInClassInitializer()));
     } else {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     return true;
   }
@@ -561,21 +564,16 @@ class GetKastVisitor
   }
 
   void VisitAccessSpecifier(AccessSpecifier Spec) {
-    const char *spec;
-    switch (Spec) {
-      case AS_public:
-        spec = "Public";
-        break;
-      case AS_protected:
-        spec = "Protected";
-        break;
-      case AS_private:
-        spec = "Private";
-        break;
-      case AS_none:
-        spec = "NoAccessSpec";
-        break;
-    }
+    const char * const spec = [&]{
+      switch (Spec) {
+        case AS_public:    return "Public";
+        case AS_protected: return "Protected";
+        case AS_private:   return "Private";
+        case AS_none:      return "NoAccessSpec";
+      }
+      assert(false && "Unknown access specifier");
+      return (const char *)nullptr;
+    }();
     Kast::add(Kast::KApply(spec, Sort::ACCESSSPECIFIER));
   }
 
@@ -1283,7 +1281,7 @@ class GetKastVisitor
   bool VisitReturnStmt(ReturnStmt *S) {
     Kast::add(Kast::KApply("ReturnStmt", Sort::STMT, {Sort::INIT}));
     if (!S->getRetValue()) {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     return false;
   }
@@ -1344,10 +1342,11 @@ class GetKastVisitor
   }
 
   bool TraverseIfStmt(IfStmt *S) {
-    Kast::add(Kast::KApply("IfAStmt", Sort::ASTMT, {Sort::DECL, Sort::ASTMT, Sort::ASTMT}));
     if (VarDecl *D = S->getConditionVariable()) {
+      Kast::add(Kast::KApply("IfAStmtD", Sort::ASTMT, {Sort::DECL, Sort::ASTMT, Sort::ASTMT}));
       TRY_TO(TraverseDecl(D));
     } else {
+      Kast::add(Kast::KApply("IfAStmt", Sort::ASTMT, {Sort::EXPR, Sort::ASTMT, Sort::ASTMT}));
       TRY_TO(TraverseStmt(S->getCond()));
     }
     TRY_TO(TraverseStmt(S->getThen()));
@@ -1360,10 +1359,11 @@ class GetKastVisitor
   }
 
   bool TraverseSwitchStmt(SwitchStmt *S) {
-    Kast::add(Kast::KApply("SwitchAStmt", Sort::ASTMT, {Sort::DECL, Sort::ASTMT}));
     if (VarDecl *D = S->getConditionVariable()) {
+      Kast::add(Kast::KApply("SwitchAStmtD", Sort::ASTMT, {Sort::DECL, Sort::ASTMT}));
       TRY_TO(TraverseDecl(D));
     } else {
+      Kast::add(Kast::KApply("SwitchAStmt", Sort::ASTMT, {Sort::EXPR, Sort::ASTMT}));
       TRY_TO(TraverseStmt(S->getCond()));
     }
     TRY_TO(TraverseStmt(S->getBody()));
@@ -1444,19 +1444,23 @@ class GetKastVisitor
 
   bool TraverseCallExpr(CallExpr *E) {
     Kast::add(Kast::KApply("CallExpr", Sort::RESOLVEDEXPR, {Sort::EXPR, Sort::STRICTLIST, Sort::STRICTLISTRESULT}));
-    unsigned i = 0;
-    for (Stmt *SubStmt : E->children()) {
-      i++;
-    }
-    if (i-1 != E->getNumArgs()) {
-      throw std::logic_error("unimplemented: pre_args???");
-    }
-    bool first = true;
-    for (Stmt *SubStmt : E->children()) {
-      TRY_TO(TraverseStmt(SubStmt));
-      if (first) List(i-1);
-      first = false;
-    }
+
+    // 1
+    TRY_TO(TraverseStmt(E->getCallee()));
+
+    // 2
+    Kast::add(Kast::KApply("list", Sort::STRICTLIST, {Sort::LIST}));
+	for (unsigned int i = 0; i < E->getNumArgs(); i++) {
+	    clang::Expr * arg = E->getArg(i);
+		if (!isa<CXXDefaultArgExpr>(arg)) {
+            Kast::add(Kast::KApply("_List_", Sort::LIST, {Sort::LIST, Sort::LIST}));
+            Kast::add(Kast::KApply("ListItem", Sort::LIST, {Sort::KITEM}));
+            TRY_TO(TraverseStmt(arg));
+        }
+	}
+    Kast::add(Kast::KApply(".List", Sort::LIST));
+
+    // 3
     Kast::add(Kast::KApply("krlist", Sort::STRICTLISTRESULT, {Sort::LIST}));
     Kast::add(Kast::KApply(".List", Sort::LIST));
     return true;
@@ -1503,7 +1507,7 @@ class GetKastVisitor
     switch (Kind) {
       #define OVERLOADED_OPERATOR(Name,Spelling,Token,Unary,Binary,MemberOnly) \
       case OO_##Name:                                                          \
-        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID));                                 \
+        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID));                                 \
         break;
       #include "clang/Basic/OperatorKinds.def"
       default:
@@ -1515,7 +1519,7 @@ class GetKastVisitor
     switch (Kind) {
       #define UNARY_OP(Name, Spelling)         \
       case UO_##Name:                          \
-        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \
+        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \
         break;
       UNARY_OP(PostInc, "_++")
       UNARY_OP(PostDec, "_--")
@@ -1548,7 +1552,7 @@ class GetKastVisitor
     switch (Kind) {
       #define BINARY_OP(Name, Spelling)        \
       case BO_##Name:                          \
-        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \
+        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \
         break;
       BINARY_OP(PtrMemD, ".*")
       BINARY_OP(PtrMemI, "->*")
@@ -1838,7 +1842,7 @@ class GetKastVisitor
     if (E->hasInitializer()) {
       TRY_TO(TraverseStmt(E->getInitializer()));
     } else {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     KSeqList(E->getNumPlacementArgs());
     for (unsigned i = 0; i < E->getNumPlacementArgs(); i++) {
@@ -2022,7 +2026,7 @@ class GetKastVisitor
 
   bool TraverseInitListExpr(InitListExpr *E) {
     InitListExpr *Syntactic = E->isSemanticForm() ? E->getSyntacticForm() ? E->getSyntacticForm() : E : E;
-    Kast::add(Kast::KApply("BraceInit", Sort::BRACEINIT, {Sort::LIST}));
+    Kast::add(Kast::KApply("BraceInit", Sort::INIT, {Sort::LIST}));
     KSeqList(Syntactic->getNumInits());
     for (Stmt *SubStmt : Syntactic->children()) {
       TRY_TO(TraverseStmt(SubStmt));
@@ -2250,7 +2254,7 @@ class GetKastVisitor
       VisitUnsigned(presumed.getColumn());
       VisitBool(mgr.isInSystemHeader(loc));
     } else {
-      Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC));
+      Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC));
     }
   }
 
diff --git a/scripts/RV_Kcc/Opts.pm b/scripts/RV_Kcc/Opts.pm
index fc93e8d52..70045e3b0 100644
--- a/scripts/RV_Kcc/Opts.pm
+++ b/scripts/RV_Kcc/Opts.pm
@@ -447,7 +447,9 @@ sub parseOpts {
 			for GCC.
       { RV_Kcc::Opts::pushArg('cppArgs', "-d$chars"); }
   -ftranslation-depth=<depth>	Compile program up to a given depth. [undocumented]
+  -fdebug-translation	Run translation semantics with GDB. [undocumented]
   -flinking-depth=<depth>	Link program up to a given depth. [undocumented]
+  -fdebug-linking	Run linking semantics with GDB. [undocumented]
   -fmessage-length=0	Write all error messages on a single line.
   -frunner-script	Compile program to perl script with analysis tool options. [undocumented]
   -fissue-report=<file>	Write issues to the specified file.
diff --git a/scripts/RV_Kcc/Shell.pm b/scripts/RV_Kcc/Shell.pm
index 2590be447..67fc5bcfd 100644
--- a/scripts/RV_Kcc/Shell.pm
+++ b/scripts/RV_Kcc/Shell.pm
@@ -11,12 +11,12 @@ use File::Spec::Functions qw(catfile);
 use String::ShellQuote qw(shell_quote_best_effort);
 use Exporter;
 
-use RV_Kcc::Files qw(tempFile kBinDir IS_CYGWIN);
+use RV_Kcc::Files qw(profileDir tempFile kBinDir IS_CYGWIN);
 
 use constant NULL => '/dev/null';
 
-use constant KBIN2TEXT         => do {
-	my $path = kBinDir('k-bin-to-text');
+use constant KAST         => do {
+	my $path = kBinDir('kast');
 	my $ext = IS_CYGWIN? '.bat' : '';
 	$path . $ext;
 };
@@ -30,6 +30,7 @@ our @EXPORT_OK = qw(
       enableDebugging
       saveArgv
       setShellDebugFile
+      setLanguageDefinition
       shell
       debug
 );
@@ -48,18 +49,24 @@ sub debug {
       }
 }
 
-sub shell {
-      my ($cmd, @args) = @_;
+sub shell_ex {
+      my ($out, $err, $cmd, @args) = @_;
       my $self =
             { CMD => $cmd
             , ARGS => \@args
-            , STDOUT => NULL
-            , STDERR => NULL
+            , STDOUT => $out
+            , STDERR => $err
             , TMP => ''
             };
       return (bless $self);
 }
 
+sub shell {
+      my ($cmd, @args) = @_;
+      return shell_ex(NULL, NULL, $cmd, @args)
+
+}
+
 sub verbose {
       my ($self) = @_;
       $self->{STDOUT} = '';
@@ -167,11 +174,20 @@ sub commandName {
             ($debugFile, $isBinary) = @_;
       }
 
+      my $languageDefinition;
+      sub setLanguageDefinition {
+            ($languageDefinition) = @_;
+      }
+
       sub checkError {
             my ($retval) = @_;
             if ($retval) {
                   if ($debugFile && $isBinary) {
-                        shell(KBIN2TEXT, $debugFile, 'kcc_config')->result();
+                        shell_ex('kcc_config', NULL, KAST,
+                          '-i', 'kore',
+                          '-o', 'pretty',
+                          '-d', $languageDefinition,
+                          $debugFile)->result();
                   } elsif ($debugFile) {
                         copy($debugFile, 'kcc_config');
                   }
diff --git a/scripts/kcc b/scripts/kcc
index cf0e0b17b..dbc39a7c7 100755
--- a/scripts/kcc
+++ b/scripts/kcc
@@ -20,7 +20,7 @@ use RV_Kcc::Opts qw(
       cppArgs suppressions ifdefs ldArgs nativeObjFiles srcFiles objFiles trampolineFiles breakpoints
       RVMAIN BASE_LIBS MAGIC
 );
-use RV_Kcc::Shell qw(shell checkError setShellDebugFile saveArgv debug);
+use RV_Kcc::Shell qw(shell checkError setShellDebugFile setLanguageDefinition saveArgv debug);
 
 # Here we trap control-c (and others) so we can clean up when that happens.
 $SIG{'ABRT'} = 'interruptHandler';
@@ -37,6 +37,8 @@ use constant KRUN         => do {
       my $ext = IS_CYGWIN? '.bat' : '';
       $path . $ext;
 };
+
+use constant LLVM_KRUN => kBinDir('llvm-krun');
 use constant PRINTF       => IS_CYGWIN? 'printf %%s' : 'printf %s';
 use constant QUOTE_INT    => IS_CYGWIN? printable("\"Int\"") : "\"Int\"";
 use constant QUOTE_STRING => IS_CYGWIN? printable("\"String\"") : "\"String\"";
@@ -127,7 +129,7 @@ sub main {
             close(FILE);
 
             my $profDir = profileDir();
-            my $krun = KRUN;
+            my $krun = LLVM_KRUN;
             $template =~ s?__EXTERN_SCRIPTS_DIR__?$profDir?g;
             $template =~ s?__EXTERN_HEAP_SIZE__?$heapSize?g;
             $template =~ s?__EXTERN_KRUN__?$krun?g;
@@ -292,15 +294,15 @@ sub makeOptions {
       my @options = ();
 
       if (arg('-fno-native-compilation')) {
-            push(@options, "`NoNativeFallback`(.KList)");
+            push(@options, "LblNoNativeFallback{}()");
       }
 
       if (arg('-frecover-all-errors')) {
-            push(@options, "`RecoverAll`(.KList)");
+            push(@options, "LblRecoverAll{}()");
       }
 
       if (arg('-fuse-native-std-lib')) {
-            push(@options, "`UseNativeStdLib`(.KList)");
+            push(@options, "LblUseNativeStdLib{})");
       }
 
       if (arg('-flint') || arg('-Wlint')) {
@@ -334,38 +336,38 @@ sub makeOptions {
                   $stackSize = printable($stackSize);
             }
             my $int = QUOTE_INT;
-            push(@options, "`Lint`(.KList)");
-            push(@options, "`Heap`(#token($heapSize, $int))");
-            push(@options, "`Stack`(#token($stackSize, $int))");
+            push(@options, "LblLint{}()");
+            push(@options, "LblHeap{}(\\dv{SortInt{}}($heapSize))");
+            push(@options, "LblStack{}(\\dv{SortInt{}}($stackSize))");
       }
 
       if (arg('-e')) {
             my $entry = quote(printable(quote(arg('-e'))));
             my $string = QUOTE_STRING;
-            push(@options, "`EntryPoint`(#token($entry, $string))");
+            push(@options, "LblEntryPoint{}(\\dv{SortString{}}($entry))");
       }
 
       if (arg('-finteractive-fail')) {
-            push(@options, "`InteractiveFail`(.KList)");
+            push(@options, "LblInteractiveFail{}()");
       }
 
       if (arg('-Wfatal-errors')) {
-            push(@options, "`FatalErrors`(.KList)");
+            push(@options, "LblFatalErrors{}()");
       }
 
       if (arg('-funresolved-symbols=')) {
             my $string_arg = arg('-funresolved-symbols=');
             if ($string_arg eq 'ignore-all') {
-                  push(@options, "`UnresolvedSymbols`(`IgnoreAll`(.KList))");
+                  push(@options, "LblUnresolvedSymbols{}(LblIgnoreAll{}())");
             } elsif ($string_arg eq 'warn-all') {
-                  push(@options, "`UnresolvedSymbols`(`WarnAll`(.KList))");
+                  push(@options, "LblUnresolvedSymbols{}(LblWarnAll{}())");
             } elsif ($string_arg eq 'report-all') {
-                  push(@options, "`UnresolvedSymbols`(`ReportAll`(.KList))");
+                  push(@options, "LblUnresolvedSymbols{}(LblReportAll{}())");
             } elsif ($string_arg eq 'warn-unreachable') {
-                  push(@options, "`UnresolvedSymbols`(`WarnUnreachable`(.KList))");
+                  push(@options, "LblUnresolvedSymbols{}(LblWarnUnreachable{}())");
             }
       } else {
-            push(@options, "`UnresolvedSymbols`(`WarnUnreachable`(.KList))");
+            push(@options, "LblUnresolvedSymbols{}(LblWarnUnreachable{}())");
       }
 
       for (breakpoints()) {
@@ -373,22 +375,22 @@ sub makeOptions {
             $file = quote(printable(quote(rel2abs($file))));
             $line = quote(printable($line));
             my ($string, $int) = (QUOTE_STRING, QUOTE_INT);
-            push(@options, "`Breakpoint`(#token($file, $string), #token($line, $int))");
+            push(@options, "LblBreakpoint{}(\\dv{SortString{}}($file), \\dv{SortInt{}}($line))");
       }
 
       if ($link) {
-            push(@options, "`Link`(.KList)");
+            push(@options, "LblLink{}()");
       }
 
-      return makeSet(@options);
+      return makeOptionSet(@options);
 
 }
 
 sub addArg {
-      my ($name, $value, $category, @krunArgs) = @_;
+      my ($name, $value, $sort, $category, @krunArgs) = @_;
 
       if (useInterpreter()) {
-            push(@krunArgs, '-c', $name, $value, $category);
+            push(@krunArgs, '-c', $name, $value, $sort, $category);
       } else {
             push(@krunArgs, "-c$name=$value");
             if ($category eq 'text' or $category eq 'binary') {
@@ -429,7 +431,7 @@ sub linkAll {
 }
 
 sub getKRunCommand {
-      my ($output, $symbols, $sem) = @_;
+      my ($output, $sem) = @_;
 
       my $def = profileDir($sem);
 
@@ -437,11 +439,14 @@ sub getKRunCommand {
       if (useInterpreter()) {
             my $dir = catfile($def, $sem);
             @krun =
-                  ( catfile($dir, 'interpreter')
-                  , catfile($dir, 'realdef.cma')
-                  , $symbols
+                  ( LLVM_KRUN
+	          , '-d'
+		  , $dir
                   , '--output-file', $output
                   );
+            if (arg('-d')) {
+                  push(@krun, '-save-temps');
+            }
       } else {
             @krun =
                   ( KRUN
@@ -450,7 +455,6 @@ sub getKRunCommand {
                   , '-d', $def
                   , '-w', 'none'
                   , '--smt', 'none'
-                  , '--argv', $symbols
                   );
 
             if (arg('-d')) {
@@ -466,23 +470,27 @@ sub getLinkingCommand {
 
       my @objs = objFiles();
 
-      my @krun = getKRunCommand($output, $symbols, 'c-cpp-linking-kompiled');
+      my @krun = getKRunCommand($output, 'c-cpp-linking-kompiled');
 
       if (arg('-flinking-depth=')) {
             push(@krun, '--depth');
             push(@krun, arg('-flinking-depth='));
       }
 
+      if (arg('-fdebug-linking')) {
+            push(@krun, '--debug');
+      }
+
       my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING);
-      my $json = "#token($rvErrorJson, $string)";
+      my $json = "\\dv{SortString{}}($rvErrorJson)";
 
-      @krun = addArg("OPTIONS", makeOptions($link), 'text', @krun);
-      @krun = addArg("JSON", $json, 'text', @krun);
+      @krun = addArg("OPTIONS", makeOptions($link), 'Set', 'kore', @krun);
+      @krun = addArg("JSON", $json, 'String', 'kore', @krun);
 
       my $uuid = create_uuid_as_string();
       my $encodedUuid = quote(printable(quote($uuid)));
-      my $uuidOpt = "#token($encodedUuid, $string)";
-      @krun = addArg("UUID", $uuidOpt, 'text', @krun);
+      my $uuidOpt = "\\dv{SortString{}}($encodedUuid)";
+      @krun = addArg("UUID", $uuidOpt, 'String', 'kore', @krun);
 
       if (scalar @objs) {
             my $allObjsFile = tempFile('all-objs');
@@ -498,29 +506,25 @@ sub getLinkingCommand {
                         };
                   }
                   if (length $thisObj) {
-                        # push(@objTexts, "`unwrapObj`($thisObj)");
-                        $thisObj = substr($thisObj, 8, -1);
                         # wrap $thisObj with `unwrapObj`()
-                        push(@objTexts, "$thisObj\x02\x00\x00\x00\x00\x00\x00\x00\x09\x00u\x00n\x00w\x00r\x00a\x00p\x00O\x00b\x00j\x00\x00\x00\x00\x01");
+                        push(@objTexts, "LblunwrapObj{}($thisObj)");
                   }
             }
-            my $objText = join('', @objTexts);
-            my $one = chr((scalar @objTexts >> 24) & 0xff);
-            my $two = chr((scalar @objTexts >> 16) & 0xff);
-            my $three = chr((scalar @objTexts >> 8) & 0xff);
-            my $four = chr((scalar @objTexts >> 0) & 0xff);
-            $objText = MAGIC . "\x04\x00\x01$objText\x03$one$two$three$four\x07";
+            my $objText = 'dotk{}()';
+	    foreach my $obj (@objTexts) {
+              $objText = 'kseq{}(' . $obj . ', ' . $objText . ')';
+	    }
+            $objText = "Lblload{}($objText)";
             open(my $file, '>', "$allObjsFile");
             print $file $objText;
             close $file;
 
-            @krun = addArg("OBJS", $allObjsFile, 'binaryfile', @krun);
+            @krun = addArg("OBJS", $allObjsFile, 'KItem', 'korefile', @krun);
       } else {
-            @krun = addArg("OBJS", ".K", 'text', @krun);
+            @krun = addArg("OBJS", "Lblload{}(dotk{}())", 'KItem', 'text', @krun);
       }
 
-      @krun = addArg("PGM", ".K", 'text', @krun);
-
+      setLanguageDefinition(profileDir('c-cpp-linking-kompiled'));
       setShellDebugFile($output, 1);
       return @krun;
 }
@@ -531,27 +535,32 @@ sub getTranslationCommand {
       my $cTransDef = profileDir("c-translation-kompiled");
       my $cppTransDef = profileDir("cpp-translation-kompiled");
 
-      my @krun = getKRunCommand($output, 'dummy',
-            $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled');
+      my $def = $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled';
+      my @krun = getKRunCommand($output, $def);
 
       if (arg('-ftranslation-depth=')) {
             push(@krun, '--depth');
             push(@krun, arg('-ftranslation-depth='));
       }
 
+      if (arg('-fdebug-translation')) {
+            push(@krun, '--debug');
+      }
+
       my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING);
-      my $json = "#token($rvErrorJson, $string)";
+      my $json = "\\dv{SortString{}}($rvErrorJson)";
 
-      @krun = addArg("OPTIONS", makeOptions(0), 'text', @krun);
-      @krun = addArg("JSON", $json, 'text', @krun);
+      @krun = addArg("OPTIONS", makeOptions(0), 'Set', 'kore', @krun);
+      @krun = addArg("JSON", $json, 'String', 'kore', @krun);
 
       my $encodedUuid = quote(printable(quote($uuid)));
-      my $uuidOpt = "#token($encodedUuid, $string)";
-      @krun = addArg("UUID", $uuidOpt, 'text', @krun);
+      my $uuidOpt = "\\dv{SortString{}}($encodedUuid)";
+      @krun = addArg("UUID", $uuidOpt, 'String', 'kore', @krun);
 
       my $kast = parse($src, $lang, $trampolines);
-      @krun = addArg("PGM", $kast, 'textfile', @krun);
+      @krun = addArg("PGM", $kast, 'KItem', 'korefile', @krun);
 
+      setLanguageDefinition(profileDir($def));
       setShellDebugFile($output, 1);
       return @krun;
 }
@@ -622,12 +631,12 @@ sub parse {
                   push(@cppParserArgs, '-fno-diagnostics-color');
             }
 
-            shell($cppParser, $ppResult, '--', @cppParserArgs)->verbose()->stdout($kast)->run();
+            shell($cppParser, $ppResult, '--kore', '--', @cppParserArgs)->verbose()->stdout($kast)->run();
 
             return $kast;
       }
       my $cparser = distDir('cparser');
-      shell($cparser, $ppResult, '--trueName', $inputFile)->verbose()->stdout($kast)->run();
+      shell($cparser, $ppResult, '--kore', '--trueName', $inputFile)->verbose()->stdout($kast)->run();
 
       return $kast;
 }
@@ -656,16 +665,16 @@ sub getStd {
       return "-std=$std";
 }
 
-sub makeSet {
-      my $set = '`.Set`(.KList)';
+sub makeOptionSet {
+      my $set = "Lbl'Stop'Set{}()";
       foreach my $el (@_) {
-            $set = "`_Set_`(`SetItem`($el), $set)";
+            $set = "Lbl'Unds'Set'Unds'{}(LblSetItem{}(inj{SortOpt{}, SortKItem{}}($el)), $set)";
       }
       return $set;
 }
 
 sub useInterpreter {
-      -e profileDir('cpp-translation-kompiled', 'cpp-translation-kompiled', 'interpreter');
+      return 1;
 }
 
 sub getRVErrorJson {
diff --git a/scripts/program-runner b/scripts/program-runner
index f9dff59b3..63cf81856 100755
--- a/scripts/program-runner
+++ b/scripts/program-runner
@@ -8,6 +8,7 @@ use File::Temp;
 use File::Copy;
 use MIME::Base64;
 use String::Escape qw(quote backslash); 
+use String::ShellQuote qw(shell_quote_best_effort);
 
 setpgrp;
 
@@ -31,9 +32,9 @@ my $SCRIPTS_DIR = '__EXTERN_SCRIPTS_DIR__';
 
 my $KRUN = '__EXTERN_KRUN__';
 
-my $EXEC_DEF = catfile($SCRIPTS_DIR, "c-cpp-kompiled");
-my $EXEC_ND_DEF = catfile($SCRIPTS_DIR, "c-nd-kompiled");
-my $EXEC_ND_THREAD_DEF = catfile($SCRIPTS_DIR, "c-nd-thread-kompiled");
+my $EXEC_DEF = catfile(catfile($SCRIPTS_DIR, "c-cpp-kompiled"), "c-cpp-kompiled");
+my $EXEC_ND_DEF = catfile(catfile($SCRIPTS_DIR, "c-nd-kompiled"), "c-nd-kompiled");
+my $EXEC_ND_THREAD_DEF = catfile(catfile($SCRIPTS_DIR, "c-nd-thread-kompiled"), "c-nd-thread-kompiled");
 
 my @temporaryFiles = ();
 
@@ -64,10 +65,9 @@ sub main {
         $objInput = '';
       }
 
-      my $argv = reduce { our ($a, $b); "`_List_`($a,$b)" } (map {qq|`ListItem`(#token($_, "String"))|} (map {quote(backslash(quote(backslash($_))))} ($0, @ARGV)));
+      my $argv = reduce { our ($a, $b); "Lbl'Unds'List'Unds'{}($a,$b)" } (map {qq|LblListItem{}(inj{SortString{}, SortKItem{}}(\\dv{SortString{}}($_)))|} (map {quote(backslash($_))} ($0, @ARGV)));
 
-      my @cmd = ('--output', 'kast', '--no-sort-collections', '--no-alpha-renaming', '-d', $EXEC_DEF, "-cARGV=$argv", '-pARGV=printf %s', '-w', 'none', '--parser',
-                 'cat', $fileInput);
+      my @cmd = ('-d', $EXEC_DEF, "-c", "ARGV", $argv, "List", "kore", "-c", "PGM", $fileInput, "GeneratedTopCell", "korefile");
       my $options = getOptions();
 
       if (defined $ENV{HELP}) {
@@ -84,73 +84,40 @@ sub main {
             return 1;
       }
 
-      if (defined $ENV{TRACE}) {
-           push @cmd, '--trace';
-      }
-
       if (defined $ENV{DEBUG}) {
            push @cmd, '--debug';
       }
 
-      if (defined $ENV{VERBOSE}) {
-           push @cmd, '--verbose';
-      }
-
-      push @cmd, '--native-libraries';
-      my $libs = nativeLibraries();
+      #push @cmd, '--native-libraries';
+      #my $libs = nativeLibraries();
       # kcc may have been run as k++ so this is necessary
-      push @cmd, "-lstdc++ $libs $objInput";
+      #push @cmd, "-lstdc++ $libs $objInput";
 
       if (defined $ENV{DEPTH}) {
             push @cmd, '--depth';
             push @cmd, $ENV{DEPTH};
       }
 
-      if (defined $ENV{PROVE}) {
-            push @cmd, '--prove';
-            push @cmd, $ENV{PROVE};
-            push @cmd, '--smt_prelude';
-            push @cmd, $ENV{SMT_PRELUDE};
-      } else {
-            push @cmd, '--smt';
-            push @cmd, 'none';
-            push @cmd, '--output-file';
-            push @cmd, $fileOutput;
-      }
-
-      if (defined $ENV{SEARCH}) {
-            push @cmd, '--search-final';
-            $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)";
-            push @cmd, '-d';
-            push @cmd, $EXEC_ND_DEF;
-            print 'Searching reachable states... ';
-            print "(with non-deterministic expression sequencing)\n";
-      }
-
-      if (defined $ENV{THREADSEARCH}) {
-            push @cmd, '--search-final';
-            $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)";
-            push @cmd, '-d';
-            push @cmd, $EXEC_ND_THREAD_DEF;
-            print 'Searching reachable states... ';
-            print "(with non-deterministic thread interleaving)\n";
-      }
+      push @cmd, '--output-file';
+      push @cmd, $fileOutput;
 
       my $encodedJson = getJson();
 
-      push @cmd, "-cOPTIONS=$options";
-      push @cmd, '-pOPTIONS=printf %s';
-      push @cmd, '-cJSON=#token(' . $encodedJson . ', "String")';
-      push @cmd, '-pJSON=printf %s';
+      push @cmd, "-c";
+      push @cmd, "OPTIONS";
+      push @cmd, $options;
+      push @cmd, "Set";
+      push @cmd, "kore";
+      push @cmd, "-c";
+      push @cmd, "JSON";
+      push @cmd, "\\dv{SortString{}}($encodedJson)";
+      push @cmd, "String";
+      push @cmd, "kore";
 
       # Execute krun with the arguments in @cmd
-      print("'krun' '" . join("' '", @cmd) . "'\n") if defined $ENV{VERBOSE};
+      print(join(' ', ($KRUN, map {shell_quote_best_effort($_)} @cmd)) . "\n") if defined $ENV{VERBOSE};
       my $ret = system($KRUN, @cmd) >> 8;
 
-      if (defined $ENV{LTLMC} | defined $ENV{PROVE}) {
-            return 0;
-      }
-
       return processResult($fileOutput, $ret, defined $ENV{VERBOSE});
 }
 
diff --git a/semantics/Makefile b/semantics/Makefile
index e79ca7e21..3ebc11bd2 100644
--- a/semantics/Makefile
+++ b/semantics/Makefile
@@ -8,9 +8,7 @@ OUTPUT_DIR := $(abspath $(BUILD_DIR))
 PROFILE_DIR := $(realpath $(CURDIR)/../profiles/x86-gcc-limited-libc)
 
 # Appending to whatever the environment provided.
-KOMPILE_FLAGS += --backend ocaml
-KOMPILE_FLAGS += --non-strict
-KOMPILE_FLAGS += --smt none
+KOMPILE_FLAGS += --backend llvm
 
 # Generate a makefile list from a colon-separated one.
 # K_INCLUDE_PATH comes from the environment.
@@ -29,6 +27,7 @@ KOMPILE_FLAGS += --no-prelude
 KOMPILE_FLAGS += -w all
 KOMPILE_FLAGS += -v
 KOMPILE_FLAGS += --debug
+KOMPILE_FLAGS += -ccopt -g
 
 
 # Used specifically in the timestamp_of rules.
diff --git a/semantics/c/language/common/check-use.k b/semantics/c/language/common/check-use.k
index 22962ed98..316ae1e6e 100644
--- a/semantics/c/language/common/check-use.k
+++ b/semantics/c/language/common/check-use.k
@@ -3,7 +3,7 @@ module C-CHECK-USE-SYNTAX
      imports SYMLOC-SORTS
 
      syntax KItem ::= checkUse(KItem) [strict]
-     syntax KItem ::= checkLoc(SymLoc)
+     syntax K ::= checkLoc(SymLoc) [function]
 
 endmodule
 
@@ -43,21 +43,18 @@ module C-CHECK-USE
           [structural]
 
      syntax Error ::= "errorLinkUnresolved"
-     rule <k> checkLoc(loc(Base:LinkBase, _))
+     rule checkLoc(loc(Base:LinkBase, _))
                => EXT-UNDEF("TDR2", "No definition for symbol with external linkage.")
                ~> errorLinkUnresolved
-          ...</k>
           requires currentSemantics() ==K ExecutionSemantics()
-          [structural]
-     rule <k> checkLoc(loc(Base:LinkBase, _, _))
+
+     rule checkLoc(loc(Base:LinkBase, _, _))
                => EXT-UNDEF("TDR2", "No definition for symbol with external linkage.")
                ~> errorLinkUnresolved
-          ...</k>
           requires currentSemantics() ==K ExecutionSemantics()
-          [structural]
-     rule <k> checkLoc(Loc::SymLoc) => checkLocAllowLink(Loc)
-          ...</k>
-          [structural, owise]
+
+     rule checkLoc(Loc::SymLoc) => checkLocAllowLink(Loc)
+          [owise]
 
      syntax KItem ::= checkLocAllowLink(SymLoc)
 
diff --git a/semantics/common/compat.k b/semantics/common/compat.k
index 792c58016..7dcde9d3b 100644
--- a/semantics/common/compat.k
+++ b/semantics/common/compat.k
@@ -28,7 +28,7 @@ module COMPAT-SYNTAX
 
      syntax List ::= removeListItem(List, K) [function]
 
-     syntax StrictListResult ::= krlist(List)
+     syntax StrictListResult ::= krlist(List) [symbol]
      syntax StrictList ::= StrictListResult
      syntax KResult ::= StrictListResult
 
diff --git a/semantics/common/configuration.k b/semantics/common/configuration.k
index 7ecccd4be..a482f4cc5 100644
--- a/semantics/common/configuration.k
+++ b/semantics/common/configuration.k
@@ -6,6 +6,9 @@ module COMMON-CONFIGURATION
   imports STRING-SYNTAX
   imports COMMON-SYNTAX
 
+  syntax Enum ::= DummyEnum()
+  syntax Class ::= DummyClass()
+
   configuration
   <global>
      <mem> .Map </mem>
@@ -101,7 +104,7 @@ module COMMON-CONFIGURATION
 
                <classes color="lightgray">
                     <class multiplicity="*" type="Map">
-                         <class-id> .K </class-id>
+                         <class-id> DummyClass() </class-id>
                          <class-type> .K </class-type>
                          <is-aggregate> true </is-aggregate>
                          <base-classes> .List </base-classes>
@@ -127,7 +130,7 @@ module COMMON-CONFIGURATION
 
                <cpp-enums>
                     <cppenum multiplicity="*" type="Map">
-                         <enum-id> .K </enum-id>
+                         <enum-id> DummyEnum() </enum-id>
                          <enum-type> .K </enum-type>
                          <scoped> false </scoped>
                          <enumerators> .Map </enumerators>
diff --git a/semantics/common/error.k b/semantics/common/error.k
index 715c669df..6b07b8418 100644
--- a/semantics/common/error.k
+++ b/semantics/common/error.k
@@ -20,7 +20,7 @@ module ERROR-SYNTAX
      syntax ErrorResult ::= errorFuncResult(K, K)
 
      syntax Error
-     syntax K ::= assert(Bool, Error)
+     syntax KItem ::= assert(Bool, Error)
 
      syntax KItem ::= "EXT" "-" "UNDEF" "(" String "," String ")" [function, klabel(LinkUndef)]
      syntax KItem ::= "EXT" "-" "UNDEF" "(" String "," String "," List ")"
@@ -47,6 +47,6 @@ module ERROR
 
      rule errorFuncResult(K1:K, K2:K) => K1 ~> K2
 
-     rule assert(B::Bool, E::Error) => #if B #then .K #else E #fi [macro]
+     rule assert(B::Bool, E::Error) => #if B #then .K #else E #fi
 
 endmodule
diff --git a/semantics/common/options.k b/semantics/common/options.k
index 3b2233cee..a67d82455 100644
--- a/semantics/common/options.k
+++ b/semantics/common/options.k
@@ -12,7 +12,7 @@ module OPTIONS-SYNTAX
                                    | WarnAll() [symbol]
                                    | WarnUnreachable() [symbol]
 
-     syntax String ::= showUnresolvedSymbolsOpt(UnresolvedSymbolsOpt)
+     syntax String ::= showUnresolvedSymbolsOpt(UnresolvedSymbolsOpt) [function]
 
      syntax Opt ::= Debug() [symbol]
                   | Link() [symbol]                         // Resolve uses to definitions.
diff --git a/semantics/common/syntax.k b/semantics/common/syntax.k
index 7e9acf661..b1d24cc20 100644
--- a/semantics/common/syntax.k
+++ b/semantics/common/syntax.k
@@ -52,7 +52,7 @@ module COMMON-SYNTAX
      syntax Bool ::= Quals "<=Quals" Quals [function]
      syntax Bool ::= Quals ">Quals" Quals [function]
 
-     syntax Namespace ::= GlobalNamespace()
+     syntax Namespace ::= GlobalNamespace() [symbol]
 
      syntax Scope ::= "none" | FileScope
      syntax FileScope ::= "fileScope"
diff --git a/semantics/cpp/language/common/class.k b/semantics/cpp/language/common/class.k
index f7508ac93..c8e9f050d 100644
--- a/semantics/cpp/language/common/class.k
+++ b/semantics/cpp/language/common/class.k
@@ -169,9 +169,9 @@ module CPP-CLASS-SYNTAX
 
      syntax Expr ::= evalBraceOrEqualInitializer(class: Class, object: Expr, initializer: Expr) [strict(c; 2)]
 
-     syntax KItem ::= returnFromBraceOrEqualInitializer(LVal, Scope)
+     syntax KItem ::= returnFromBraceOrEqualInitializer(Expr, Scope)
 
-     syntax This ::= This()
+     syntax This ::= This() [symbol]
 
      syntax Expr ::= This
 
diff --git a/semantics/cpp/language/common/conversion.k b/semantics/cpp/language/common/conversion.k
index ec4aeb862..c36b6f666 100644
--- a/semantics/cpp/language/common/conversion.k
+++ b/semantics/cpp/language/common/conversion.k
@@ -6,9 +6,7 @@ module CPP-CONVERSION-SYNTAX
      syntax Expr ::= instantiate(SymLoc, Trace, CPPType) [klabel(instantiateCpp)]
 
      // performs standard type conversions only
-     syntax PRVal ::= convertType(CPPType, PRVal) [function]
-
-     syntax PRExpr ::= convertType(CPPType, PRExpr) [function]
+     syntax Expr ::= convertType(CPPType, Expr) [function]
 
      syntax Expr ::= convertTypeHold(CPPType, Expr)
 
@@ -216,7 +214,7 @@ module CPP-CONVERSION
           requires X1 ==Type X2 andBool isSimilar(T1, T2)
                andBool cvQualificationSignature(T1) <=QualSig cvQualificationSignature(T2)
 
-     rule convertType(_::CPPType, _::PRExpr) => cannot-convert [owise]
+     rule convertType(_::CPPType, _:PRExpr) => cannot-convert [owise]
 
      rule isSimilar(t(_, _, pointerType(T1::CPPType)), t(_, _, pointerType(T2::CPPType)))
           => isSimilar(T1, T2)
diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k
index 97af1464c..d2ab9a292 100644
--- a/semantics/cpp/language/common/dynamic.k
+++ b/semantics/cpp/language/common/dynamic.k
@@ -273,12 +273,12 @@ module CPP-QUALID-SYNTAX
      imports CPP-QUALID-SORTS // self
      imports CPP-SORTS // CId, Name
 
-     syntax NNS ::= NoNNS()
-                  | NNS "::" NNSSpecifier [klabel(NestedName)]
+     syntax NNS ::= NoNNS() [symbol]
+                  | NNS "::" NNSSpecifier [klabel(NestedName), symbol]
 
-     syntax NNSSpecifier ::= NNS(CId)
+     syntax NNSSpecifier ::= NNS(CId) [klabel(NNSCId), symbol]
                            | TemplateNNS(CId)
-                           | NNS(Name)
+                           | NNS(Name) [klabel(NNSName), symbol]
 
      syntax QualId ::= NNSVal "::" CId [klabel(QualId)]
 
@@ -518,7 +518,7 @@ module CPP-DYNAMIC-OTHER-SYNTAX
      syntax CPPTypes ::= toCPPTypes(List) [function]
                        | toCPPTypes(TemplateArgs) [function, klabel(TemplateArgsToCPPTypes)]
 
-     syntax TemplateArg ::= CPPType
+     syntax TemplateArg ::= CPPDType
 
      syntax String ::= showCPPTypes(CPPTypes) [function]
                      | showCPPType(CPPType) [function]
@@ -563,7 +563,7 @@ module CPP-DYNAMIC-OTHER-SYNTAX
 
      syntax KItem ::= odrDecl(String, QualId, CId, LanguageLinkage, CPPType)
 
-     syntax Stmt ::= compoundStmt(Stmt, Stmt)
+     syntax Stmt ::= compoundStmt(K, Stmt)
      syntax Stmt ::= nullStmt()
 
      syntax SSList ::= toSSList(List) [klabel(toSSListcpp), function]
@@ -777,7 +777,7 @@ module CPP-DYNAMIC-OTHER
 
      rule toTemplateArgs(.List) => .TemplateArgs
 
-     rule toCPPTypes(ListItem(A::CPPType) L::List) => A, toCPPTypes(L)
+     rule toCPPTypes(ListItem(A::CPPDType) L::List) => A, toCPPTypes(L)
 
      rule toCPPTypes(.List) => .CPPTypes
 
@@ -785,7 +785,7 @@ module CPP-DYNAMIC-OTHER
 
      rule CPPTypesSize(Ts::CPPTypes) => size(toList(Ts))
 
-     rule toList(T::CPPType, Ts::CPPTypes) => ListItem(T) toList(Ts)
+     rule toList(T::CPPDType, Ts::CPPTypes) => ListItem(T) toList(Ts)
 
      rule toList(.CPPTypes) => .List
 
@@ -1006,7 +1006,8 @@ module CPP-DYNAMIC-OTHER
      rule showTemplateArgs(T:CPPType, T2:TemplateArg, Ts::TemplateArgs)
           => showCPPType(T) +String "," +String showTemplateArgs(T2, Ts)
 
-     rule _:KResult ~> discard => .K
+     rule X:KItem ~> discard => .K
+          requires isKResult(X)
 
      context <k> makePRVal(HOLE:Expr => reval(HOLE)) ...</k> 
              <compile-time-evaluation> true </compile-time-evaluation> [result(PRV)]
@@ -1067,7 +1068,7 @@ module CPP-DYNAMIC-OTHER
 
      rule Translation() => notBool Execution()
 
-     rule compoundStmt(S1::Stmt, S2::Stmt) => S1 ~> S2
+     rule compoundStmt(S1::K, S2::Stmt) => S1 ~> S2
      rule nullStmt() => .K
 
      rule idOf(Class(_, X::CId, _)) => X
diff --git a/semantics/cpp/language/common/io.k b/semantics/cpp/language/common/io.k
index 37d8199cb..900149957 100644
--- a/semantics/cpp/language/common/io.k
+++ b/semantics/cpp/language/common/io.k
@@ -4,7 +4,7 @@ module CPP-COMMON-IO-SYNTAX
 
      syntax CPPType
 
-     syntax K ::= assertInBounds(Int, Int) [klabel(cppAssertInBounds)]
+     syntax KItem ::= assertInBounds(Int, Int) [klabel(cppAssertInBounds)]
 
      syntax Bits ::= getUninitializedBits(SymLoc, CPPType) [function, klabel(getUninitializedBitsCpp)]
 
@@ -25,7 +25,7 @@ module CPP-COMMON-IO
      syntax Error ::= "errorReadOutOfBounds"
 
      rule assertInBounds(Offset::Int, Len::Int)
-          => assert(Offset <Int Len, errorReadOutOfBounds) [macro]
+          => assert(Offset <Int Len, errorReadOutOfBounds)
 
      rule (.K => DRAFTING("EIO1",
                "Reading outside the bounds of an object."))
diff --git a/semantics/cpp/language/common/syntax.k b/semantics/cpp/language/common/syntax.k
index 2921e7d6a..6e3e0d894 100644
--- a/semantics/cpp/language/common/syntax.k
+++ b/semantics/cpp/language/common/syntax.k
@@ -101,9 +101,9 @@ module CPP-SYNTAX
 
      syntax Tag ::= ClassKey | Enum() [symbol] | Typename() [symbol] | NoTag() [symbol]
 
-     syntax AccessSpecifier ::= Public() [symbol] | Private() [symbol] | Protected() [symbol] | NoAccessSpec()
+     syntax AccessSpecifier ::= Public() [symbol] | Private() [symbol] | Protected() [symbol] | NoAccessSpec() [symbol]
 
-     syntax RefQualifier ::= RefLValue() | RefRValue() | RefNone()
+     syntax RefQualifier ::= RefLValue() [symbol] | RefRValue() [symbol] | RefNone() [symbol]
 
      syntax TemplateKeyword ::= "template" | "no-template"
 
@@ -117,8 +117,8 @@ module CPP-SYNTAX
                    | Expr "++" [strict(c)]
                    | Expr "--" [strict(c)]
                    | BuiltinCallOp(Expr, Bool, List)
-                   | ReinterpretCast(AType, Expr) [strict(c)]
-                   | ConstCast(AType, Expr) [strict(c)]
+                   | ReinterpretCast(AType, Expr) [strict(c), symbol]
+                   | ConstCast(AType, Expr) [strict(c), symbol]
                    > right:
                      "++" Expr [strict(c)]
                    | "--" Expr [strict(c)]
@@ -183,8 +183,8 @@ module CPP-SYNTAX
                    | ThrowOp(Expr) [strict(c)]
                    > left:
                      Comma(Expr, Expr) [strict(c; 1)]
-     syntax Name ::= Name(NNS, CId)
-                   | Name(NNS, CId, List)
+     syntax Name ::= Name(NNS, CId) [symbol]
+                   | Name(NNS, CId, List) [klabel(Name3)]
 
      syntax ExecName ::= ExecName(NNS, CId)
 
@@ -193,7 +193,7 @@ module CPP-SYNTAX
      syntax Expr ::= ConvertType(CPPType, Expr)
                    | ExprLoc
 
-     syntax ExprLoc ::= ExprLoc(CabsLoc, KItem)
+     syntax ExprLoc ::= ExprLoc(CabsLoc, KItem) [symbol]
 
      syntax Init ::= ExprLoc
 
@@ -203,7 +203,7 @@ module CPP-SYNTAX
      syntax Decl
 
      syntax Stmt ::= LabelStmt(CId, List)
-                   | GotoStmt(CId)
+                   | GotoStmt(CId) [symbol]
                    | ExpressionStmt(Expr) [strict(c)]
                    | PRValExpressionStmt(Expr) [strict(c)]
                    | BreakStmt()
diff --git a/semantics/cpp/language/common/typing.k b/semantics/cpp/language/common/typing.k
index 953f04b51..3edb74425 100644
--- a/semantics/cpp/language/common/typing.k
+++ b/semantics/cpp/language/common/typing.k
@@ -409,7 +409,7 @@ module CPP-TYPING
 
      rule getParams(t(_, _, functionType(... paramTypes: L::CPPTypes, methodInfo: methodInfo(... constructor: true)))) => toList(L)
 
-     rule getParams(t(_, _, functionType(... paramTypes: L::CPPTypes, methodInfo: methodInfo(RQ::RefQualifier, CVS::Quals, IsStatic::Bool, _, _, _, C::Class, _, false)))) => ListItem(implicitObjectParameter(getImpliedParamType(RQ, CVS, IsStatic, C))) toList(L)
+     rule getParams(t(_, _, functionType(... paramTypes: L::CPPTypes, methodInfo: methodInfo(RQ::RefQualifier, CVS::Quals, IsStatic::Bool, _, _, _, C::K, _, false)))) => ListItem(implicitObjectParameter(getImpliedParamType(RQ, CVS, IsStatic, C))) toList(L)
 
      rule getRealParams(T::CPPType) => #getRealParams(getParams(T))
 
@@ -451,7 +451,7 @@ module CPP-TYPING
      rule hasImplicitParameter(_) => false [owise]
 
      // TODO(traiansf): Handle conversion functions and functions introduced by using declarations
-     syntax CPPType ::= getImpliedParamType(RefQualifier, Quals, static: Bool, Class) [function]
+     syntax CPPType ::= getImpliedParamType(RefQualifier, Quals, static: Bool, class: K) [function]
 
      // 13.3.1:4
      rule getImpliedParamType(... static: true) => type(no-type)
@@ -779,6 +779,8 @@ module CPP-TYPING
 
      rule stripTypes(T::CPPType, Ts::TemplateArgs) => stripType(T), stripTypes(Ts)
 
+     rule stripTypes(variadic, Ts::TemplateArgs) => variadic, stripTypes(Ts)
+
      rule stripTypes(.TemplateArgs) => .TemplateArgs
 
      rule T1::CPPType ==Type T2::CPPType => stripType(T1) ==K stripType(T2)
@@ -975,7 +977,7 @@ module CPP-TYPING
 
      rule setType(T::CPPType, lv(Loc::SymLoc, Tr::Trace, _)) => lv(Loc, Tr, T)
 
-     rule setType(T::CPPType, prv(Loc::SymLoc, Tr::Trace, _)) => prv(Loc, Tr, T)
+     rule setType(T::CPPType, prv(V::CPPValue, Tr::Trace, _)) => prv(V, Tr, T)
 
      rule isEnumScoped(t(_, _, scopedEnum(_, _))) => true
 
diff --git a/semantics/cpp/language/execution/binding.k b/semantics/cpp/language/execution/binding.k
index febb7868f..3fe7027bf 100644
--- a/semantics/cpp/language/execution/binding.k
+++ b/semantics/cpp/language/execution/binding.k
@@ -8,7 +8,7 @@ module CPP-BINDING-SYNTAX
 
      syntax KItem ::= bindParam(CId, CPPType, Init) [klabel(bindParamCpp3)]
 
-     syntax KItem ::= setThis(Expr) [strict(c)]
+     syntax KItem ::= setThis(K)
 endmodule
 
 module CPP-EXECUTION-BINDING
@@ -23,6 +23,13 @@ module CPP-EXECUTION-BINDING
      imports CPP-SYNTAX
      imports CPP-TYPING-SYNTAX
 
+     rule <k> setThis(.K) => .K ...</k>
+          <this> _ => .K </this>
+
+     rule setThis(E:Expr) => #setThis(E)
+
+     syntax KItem ::= #setThis(Expr) [strict(c)]
+
      rule <k> (.K => bindParam(X, T, V))
           ~> bind(
                (ListItem(X::CId) => .List) _,
@@ -30,7 +37,7 @@ module CPP-EXECUTION-BINDING
                (ListItem(V::Init) => .List) _)
           ...</k>
 
-     rule <k> (.K => setThis(V))
+     rule <k> (.K => #setThis(V))
           ~> bind(
                _,
                (ListItem(implicitObjectParameter(T::CPPType)) => .List) _,
@@ -52,7 +59,7 @@ module CPP-EXECUTION-BINDING
 
      rule bindVariadics(.List) => .K
 
-     rule <k> setThis(Obj:PRVal) => .K ...</k>
+     rule <k> #setThis(Obj:PRVal) => .K ...</k>
           <this> _ => Obj </this>
 
      rule <k> beginConstruction(Obj:LVal, IsBaseClassSubobject:Bool) => Obj ...</k>
diff --git a/semantics/cpp/language/execution/expr/assignment.k b/semantics/cpp/language/execution/expr/assignment.k
index 33d15d031..b6185757b 100644
--- a/semantics/cpp/language/execution/expr/assignment.k
+++ b/semantics/cpp/language/execution/expr/assignment.k
@@ -55,21 +55,21 @@ module CPP-EXECUTION-EXPR-ASSIGNMENT
      rule compoundOp(compoundExprs(_, R::Expr) #as E:ResolvedExpr) => E
           requires isKResult(R) andBool Execution()
 
-     rule fillRHoles(V::PRVal, pre(L::Expr := E::Expr, Tr::Trace, T::CPPType)) => pre(L := fillRHoles(V, E), Tr, T)
-     rule fillRHoles(V::PRVal, V':PRV) => V'
-     rule fillRHoles(V::PRVal, ConvertType(T::CPPType, E::Expr)) => ConvertType(T, fillRHoles(V, E))
-     rule fillRHoles(V::PRVal, compoundOp(E::Expr)) => compoundOp(fillRHoles(V, E))
-     rule fillRHoles(V::PRVal, RHOLE) => V
-     rule fillRHoles(V::PRVal, L::Expr + R::Expr) => fillRHoles(V, L) + R
-     rule fillRHoles(V::PRVal, L::Expr - R::Expr) => fillRHoles(V, L) - R
-     rule fillRHoles(V::PRVal, L::Expr * R::Expr) => fillRHoles(V, L) * R
-     rule fillRHoles(V::PRVal, L::Expr / R::Expr) => fillRHoles(V, L) / R
-     rule fillRHoles(V::PRVal, L::Expr % R::Expr) => fillRHoles(V, L) % R
-     rule fillRHoles(V::PRVal, L::Expr & R::Expr) => fillRHoles(V, L) & R
-     rule fillRHoles(V::PRVal, L::Expr ^ R::Expr) => fillRHoles(V, L) ^ R
-     rule fillRHoles(V::PRVal, L::Expr | R::Expr) => fillRHoles(V, L) | R
-     rule fillRHoles(V::PRVal, L::Expr << R::Expr) => fillRHoles(V, L) << R
-     rule fillRHoles(V::PRVal, L::Expr >> R::Expr) => fillRHoles(V, L) >> R
+     rule fillRHoles(V::Expr, pre(L::Expr := E::Expr, Tr::Trace, T::CPPType)) => pre(L := fillRHoles(V, E), Tr, T)
+     rule fillRHoles(V::Expr, V':PRV) => V'
+     rule fillRHoles(V::Expr, ConvertType(T::CPPType, E::Expr)) => ConvertType(T, fillRHoles(V, E))
+     rule fillRHoles(V::Expr, compoundOp(E::Expr)) => compoundOp(fillRHoles(V, E))
+     rule fillRHoles(V::Expr, RHOLE) => V
+     rule fillRHoles(V::Expr, L::Expr + R::Expr) => fillRHoles(V, L) + R
+     rule fillRHoles(V::Expr, L::Expr - R::Expr) => fillRHoles(V, L) - R
+     rule fillRHoles(V::Expr, L::Expr * R::Expr) => fillRHoles(V, L) * R
+     rule fillRHoles(V::Expr, L::Expr / R::Expr) => fillRHoles(V, L) / R
+     rule fillRHoles(V::Expr, L::Expr % R::Expr) => fillRHoles(V, L) % R
+     rule fillRHoles(V::Expr, L::Expr & R::Expr) => fillRHoles(V, L) & R
+     rule fillRHoles(V::Expr, L::Expr ^ R::Expr) => fillRHoles(V, L) ^ R
+     rule fillRHoles(V::Expr, L::Expr | R::Expr) => fillRHoles(V, L) | R
+     rule fillRHoles(V::Expr, L::Expr << R::Expr) => fillRHoles(V, L) << R
+     rule fillRHoles(V::Expr, L::Expr >> R::Expr) => fillRHoles(V, L) >> R
 
      rule fillLHoles(LV::Expr, pre(LHOLE := R::Expr, Tr::Trace, T::CPPType))
           => pre(LV := R, Tr, T)
diff --git a/semantics/cpp/language/execution/expr/function-call.k b/semantics/cpp/language/execution/expr/function-call.k
index 264f90daf..1c46a282f 100644
--- a/semantics/cpp/language/execution/expr/function-call.k
+++ b/semantics/cpp/language/execution/expr/function-call.k
@@ -131,7 +131,7 @@ module CPP-EXECUTION-EXPR-FUNCTION-CALL
               ~> K:K
               => sequencePoint
               ~> enterRestrictBlock(blockScope(X, Base, 0))
-              ~> #if Obj ==K .K #then .K #else setThis(& Obj) #fi
+              ~> #if Obj ==K .K #then .K #else setThis(& {Obj}:>Expr) #fi
               ~> bind(Params, getParams(DefT), L)
               ~> Blk
           </k>
@@ -149,7 +149,7 @@ module CPP-EXECUTION-EXPR-FUNCTION-CALL
                </call-stack-frame>
           ) ...</call-stack>
           (<function-control> C::Bag
-               <constructing> Obj::Expr </constructing>
+               <constructing> Obj:K </constructing>
                <curr-program-loc> _ </curr-program-loc>
                <most-derived-class> MDC:K </most-derived-class>
           </function-control>
diff --git a/semantics/cpp/language/execution/expr/members.k b/semantics/cpp/language/execution/expr/members.k
index b44c53fb6..184a02717 100644
--- a/semantics/cpp/language/execution/expr/members.k
+++ b/semantics/cpp/language/execution/expr/members.k
@@ -15,10 +15,10 @@ module CPP-EXECUTION-EXPR-MEMBERS
 
      rule <k> evalBraceOrEqualInitializer(C::Class, lv(Loc::SymLoc, Tr::Trace, T::CPPType) #as Base::LVal, E::Expr) => setThis(prv(Loc, Tr, type(pointerType(type(classType(C)))))) ~> E ~> returnFromBraceOrEqualInitializer(Base, OldScope) ~> setThis(OldThis) ...</k>
           <curr-scope> OldScope::Scope => classScope(C, true) </curr-scope>
-          <this> OldThis::PRVal </this>
+          <this> OldThis::K </this>
           requires Execution()
 
-     rule <k> V:Val ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) ~> setThis(OldThis::PRVal) => .K) ...</k>
+     rule <k> V:Val ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) ~> setThis(OldThis::K) => .K) ...</k>
           <curr-scope> _ => Scope </curr-scope>
           <this> _ => OldThis </this>
           requires Execution() andBool notBool (isLExpr(V) orBool isPRExpr(V))
diff --git a/semantics/cpp/language/execution/stmt/block.k b/semantics/cpp/language/execution/stmt/block.k
index a2c521706..7dc14f03a 100644
--- a/semantics/cpp/language/execution/stmt/block.k
+++ b/semantics/cpp/language/execution/stmt/block.k
@@ -99,7 +99,7 @@ module CPP-EXECUTION-STMT-BLOCK
      rule <k> (.K => destructLocal(IsException, Entry))
               ~> destructLocals(IsException:Bool)
           ...</k>
-          <locally-constructed> ListItem(Entry::KTuple) => .List ...</locally-constructed>
+          <locally-constructed> ListItem(Entry::KItem) => .List ...</locally-constructed>
 
      rule <k> destructLocals(...) => .K ...</k>
           <locally-constructed> .List </locally-constructed>
diff --git a/semantics/cpp/language/execution/stmt/if.k b/semantics/cpp/language/execution/stmt/if.k
index e9209242e..f3ef84c45 100644
--- a/semantics/cpp/language/execution/stmt/if.k
+++ b/semantics/cpp/language/execution/stmt/if.k
@@ -9,8 +9,8 @@ module CPP-EXECUTION-STMT-IF
 
      rule IfStmt(prv((unknown(I::Int) => #if I ==Int 0 #then 0 #else 1 #fi), _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), _, _)
 
-     rule IfStmt(prv(1, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), S::Stmt, _) => fullExpression ~> S
+     rule IfStmt(prv(1, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), S::K, _) => fullExpression ~> S
 
-     rule IfStmt(prv(0, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), _, S::Stmt) => fullExpression ~> S
+     rule IfStmt(prv(0, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), _, S::K) => fullExpression ~> S
 
 endmodule
diff --git a/semantics/cpp/language/execution/stmt/loop.k b/semantics/cpp/language/execution/stmt/loop.k
index 60a0bea4a..9ddf3bc47 100644
--- a/semantics/cpp/language/execution/stmt/loop.k
+++ b/semantics/cpp/language/execution/stmt/loop.k
@@ -4,7 +4,7 @@ module CPP-EXECUTION-STMT-LOOP
      imports CPP-DYNAMIC-SYNTAX
      imports CPP-SYNTAX
 
-     rule <k> ForStmt(Control::Expr, Post::Stmt, S::Stmt) ~> K:K
+     rule <k> ForStmt(Control::Expr, Post::K, S::K) ~> K:K
               => loopMarked
               ~> ForStmt(Control, Post, S)
               ~> popLoop
@@ -12,7 +12,7 @@ module CPP-EXECUTION-STMT-LOOP
           <block-history> ListItem(Num::Int) ...</block-history>
           <loop-stack> .List => ListItem(kpair(Num, K)) ...</loop-stack>
 
-     rule loopMarked ~> ForStmt(Control:Expr, Post::Stmt, S::Stmt)
+     rule loopMarked ~> ForStmt(Control:Expr, Post::K, S::K)
           => IfStmt(Control, compoundStmt(S, compoundStmt(Post, compoundStmt(loopMarked,
               ForStmt(Control, Post, S)))), nullStmt())
 
@@ -24,7 +24,7 @@ module CPP-EXECUTION-STMT-LOOP
           <block-history> ListItem(Num::Int) ...</block-history>
           <loop-stack> .List => ListItem(kpair(Num, K)) ...</loop-stack>
 
-     rule loopMarked ~> WhileStmt(Control:Expr, S::Stmt)
+     rule loopMarked ~> WhileStmt(Control:Expr, S::K)
           => IfStmt(Control, compoundStmt(S, compoundStmt(loopMarked,
                WhileStmt(Control, S))), nullStmt())
 
diff --git a/semantics/cpp/language/execution/stmt/return.k b/semantics/cpp/language/execution/stmt/return.k
index d0b5f1061..931f05f16 100644
--- a/semantics/cpp/language/execution/stmt/return.k
+++ b/semantics/cpp/language/execution/stmt/return.k
@@ -81,7 +81,7 @@ module CPP-EXECUTION-STMT-RETURN
           (<function-control>
                <live-va-lists> .Set </live-va-lists>
                <block-stack> .List </block-stack>
-               <ret-constructed-temporary> LCE::KItem  </ret-constructed-temporary>
+               <ret-constructed-temporary> LCE::K  </ret-constructed-temporary>
           ...</function-control> => C)
           <call-stack>
                ListItem(
diff --git a/semantics/cpp/language/execution/stmt/try.k b/semantics/cpp/language/execution/stmt/try.k
index d200bc6c4..66e9acdc3 100644
--- a/semantics/cpp/language/execution/stmt/try.k
+++ b/semantics/cpp/language/execution/stmt/try.k
@@ -145,10 +145,10 @@ module CPP-EXECUTION-STMT-TRY
           requires size(S) >Int 0
 
      rule <k> throw(V::LVal) => catchWithHandler(CatchAnyOp(S), V) ...</k>
-          <catch-handlers> ListItem(CatchAnyOp(S::Stmt)) ...</catch-handlers>
+          <catch-handlers> ListItem(CatchAnyOp(S::K)) ...</catch-handlers>
 
      rule <k> throw(V::LVal) => catchWithHandler(CatchOp(T, S), V) ...</k>
-          <catch-handlers> ListItem(CatchOp(T::CPPType, S::Stmt)) ...</catch-handlers>
+          <catch-handlers> ListItem(CatchOp(T::CPPType, S::K)) ...</catch-handlers>
           requires handlerMatches(T, type(V))
 
      rule <k> throw(V::LVal) ... </k>
diff --git a/semantics/cpp/language/execution/temporary.k b/semantics/cpp/language/execution/temporary.k
index 7d24a754a..bc4e19bab 100644
--- a/semantics/cpp/language/execution/temporary.k
+++ b/semantics/cpp/language/execution/temporary.k
@@ -56,7 +56,7 @@ module CPP-EXECUTION-TEMPORARY
      rule <k> (.K => destructLocal(IsException, Entry))
               ~> destructTemporaries(IsException:Bool)
           ...</k>
-          <constructed-temporaries> ListItem(Entry::KTuple) => .List ...</constructed-temporaries>
+          <constructed-temporaries> ListItem(Entry::KItem) => .List ...</constructed-temporaries>
 
      rule <k> destructTemporaries(...) => .K ...</k>
           <constructed-temporaries> .List </constructed-temporaries>
diff --git a/semantics/cpp/language/translation/conversion.k b/semantics/cpp/language/translation/conversion.k
index 4e6ad6e7f..1507a6170 100644
--- a/semantics/cpp/language/translation/conversion.k
+++ b/semantics/cpp/language/translation/conversion.k
@@ -12,7 +12,7 @@ module CPP-TRANSLATION-CONVERSION
 
      rule convertType(t(... st: memberPointerType(...)) #as T::CPPType, prv(0, hasTrace(IntegerLiteral(0, T2::CPPType)), _)) => prv(NullMemberPointer, hasTrace(IntegerLiteral(0, T2)), T)
 
-     rule convertType(T::CPPType, pre(E::Expr, Tr::Trace, _)) => pre(ConvertType(T, E), Tr, T)
+     rule convertType(T::CPPType, pre(E:Expr, Tr::Trace, _)) => pre(ConvertType(T, E), Tr, T)
 
      rule isNullPointerConstant(prv(_, hasTrace(IntegerLiteral(0, _)), _)) => true
 
diff --git a/semantics/cpp/language/translation/decl/class.k b/semantics/cpp/language/translation/decl/class.k
index ebfec3a82..f793a021c 100644
--- a/semantics/cpp/language/translation/decl/class.k
+++ b/semantics/cpp/language/translation/decl/class.k
@@ -1471,22 +1471,22 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
      rule pad(V::Int, _) => V [owise]
 
      // brace-or-equal initializers need to be evalauted in class scope
-     rule <k> evalBraceOrEqualInitializer(C::Class, Base::LVal, E::Expr) => E ~> returnFromBraceOrEqualInitializer(Base, OldScope) ...</k>
+     rule <k> evalBraceOrEqualInitializer(C::Class, Base::Expr, E::Expr) => E ~> returnFromBraceOrEqualInitializer(Base, OldScope) ...</k>
           <curr-tr-scope> OldScope::Scope => classScope(C, true) </curr-tr-scope>
-          requires Translation()
+          requires Translation() andBool isKResult(Base)
 
      rule <k> le(E::Expr => evalBraceOrEqualInitializer(C, Base, E), _, _)
-           ~> (returnFromBraceOrEqualInitializer(Base::LVal, Scope::Scope) => .K)
+           ~> (returnFromBraceOrEqualInitializer(Base::Expr, Scope::Scope) => .K)
           ...</k>
           <curr-tr-scope> classScope(C::Class, _) => Scope </curr-tr-scope>
 
      rule <k> xe(E::Expr => evalBraceOrEqualInitializer(C, Base, E), _, _)
-           ~> (returnFromBraceOrEqualInitializer(Base::LVal, Scope::Scope) => .K)
+           ~> (returnFromBraceOrEqualInitializer(Base::Expr, Scope::Scope) => .K)
           ...</k>
           <curr-tr-scope> classScope(C::Class, _) => Scope </curr-tr-scope>
 
      rule <k> pre(E::Expr => evalBraceOrEqualInitializer(C, Base, E), _, _)
-           ~> (returnFromBraceOrEqualInitializer(Base::LVal, Scope::Scope) => .K)
+           ~> (returnFromBraceOrEqualInitializer(Base::Expr, Scope::Scope) => .K)
           ...</k>
           <curr-tr-scope> classScope(C::Class, _) => Scope </curr-tr-scope>
 
@@ -1494,20 +1494,22 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
           <curr-tr-scope> _ => Scope </curr-tr-scope>
           requires notBool (isLExpr(V) orBool isPRExpr(V))
 
-     rule <k> typeof(evalBraceOrEqualInitializer(C::Class, Base::LVal, E::Expr) => E)
-           ~> (.K => returnFromBraceOrEqualInitializer(Base, OldScope))
+     syntax KItem ::= restoreScope(Scope)
+
+     rule <k> typeof(evalBraceOrEqualInitializer(C::Class, _, E::Expr) => E)
+           ~> (.K => restoreScope(OldScope))
           ...</k>
           <curr-tr-scope> OldScope::Scope => classScope(C, true) </curr-tr-scope>
 
-     rule <k> typeof(V:CPPType) ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) => .K) ...</k>
+     rule <k> typeof(V:CPPType) ~> (restoreScope(Scope::Scope) => .K) ...</k>
           <curr-tr-scope> _ => Scope </curr-tr-scope>
 
-     rule <k> catof(evalBraceOrEqualInitializer(C::Class, Base::LVal, E::Expr) => E)
-           ~> (.K => returnFromBraceOrEqualInitializer(Base, OldScope))
+     rule <k> catof(evalBraceOrEqualInitializer(C::Class, _, E::Expr) => E)
+           ~> (.K => restoreScope(OldScope))
           ...</k>
           <curr-tr-scope> OldScope::Scope => classScope(C, true) </curr-tr-scope>
 
-     rule <k> catof(V:ValueCategory) ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) => .K) ...</k>
+     rule <k> catof(V:ValueCategory) ~> (restoreScope(Scope::Scope) => .K) ...</k>
           <curr-tr-scope> _ => Scope </curr-tr-scope>
 
      rule Class.getNonStaticDataMembers(<class>... <non-static-data-members> L::List </non-static-data-members> ...</class>) => L
diff --git a/semantics/cpp/language/translation/decl/declarator.k b/semantics/cpp/language/translation/decl/declarator.k
index 6cbc1c2f6..0d76a442d 100644
--- a/semantics/cpp/language/translation/decl/declarator.k
+++ b/semantics/cpp/language/translation/decl/declarator.k
@@ -53,13 +53,13 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      imports CPP-TRANSLATION-CONSTANT-SYNTAX
      imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR
 
-     rule FunctionDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List)
+     rule FunctionDecl(N::NNS, X::CId, Mangled::CId, T::AType, Params::List)
           => NormalizedDecl(N, X, Mangled, T, NoInit(), Function(Params)) [anywhere]
 
-     rule VarDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Init::Init, IsDirect:Bool)
+     rule VarDecl(N::NNS, X::CId, Mangled::CId, T::AType, Init::Init, IsDirect:Bool)
           => NormalizedDecl(N, X, Mangled, T, Init, Var(#if IsDirect #then DirectInit() #else CopyInit() #fi)) [anywhere]
 
-     rule FunctionDefinition(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List, Body::Stmt)
+     rule FunctionDefinition(N::NNS, X::CId, Mangled::CId, T::AType, Params::List, Body::Stmt)
           => NormalizedDecl(N, X, Mangled, T, Body, Function(Params)) [anywhere]
 
      rule DeclStmt(L::List) => listToK(L)
@@ -72,7 +72,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      rule Specifier(Spec::Specifier, DeclaratorAndSpecifiers(D::Declarator, S::Set)) => DeclaratorAndSpecifiers(D, S SetItem(Spec)) [anywhere]
 
-     rule NormalizedDecl(N::NNSVal, X::CId, Mangled::CId, T::AType, Init::Init, Type::DeclarationType)
+     rule NormalizedDecl(N::NNS, X::CId, Mangled::CId, T::AType, Init::Init, Type::DeclarationType)
           => DeclaratorAndSpecifiers(NormalizedDecl(N, X, Mangled, T, Init, Type), .Set)
 
      context DeclaratorAndSpecifiers(NormalizedDecl(... nns: HOLE:NNS), _)
@@ -115,7 +115,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      syntax Duration ::= getDuration(Set, Scope) [function]
 
-     syntax Namespace ::= getInnermostNamespace(NNSVal, Scope) [function]
+     syntax NNSVal ::= getInnermostNamespace(NNSVal, Scope) [function]
 
      rule getPreviousLinkage(X::QualId, T::CPPType, X |-> (stripType(T) |-> _ _::Map) _::Map, _) => ExternalLinkage
 
@@ -186,7 +186,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      rule getInnermostNamespace(NoNamespace(), blockScope((localQual(Scope::BlockScope) :: _:ClassSpecifier) :: _, _, _) => Scope)
 
-     rule getInnermostNamespace(N::Namespace, _) => N
+     rule getInnermostNamespace(N::NNSVal, _) => N
           requires N =/=K NoNamespace()
 
      /* After everything is computed */
@@ -403,8 +403,9 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule <k> stripAuto => .K ...</k>
           <template-arguments>... auto |-> _ => .Map ...</template-arguments>
 
-    rule declareNonStaticObject(ID::CId, T::CPPType, Init:KResult, DT::DeclarationType, DU::Duration, S::Set)
+    rule declareNonStaticObject(ID::CId, T::CPPType, Init:KItem, DT::DeclarationType, DU::Duration, S::Set)
           =>  declareNonStaticObject2(declareNonStaticObjectExec(ID, T, Init, DT, DU, S), Constexpr() in S)
+         requires isKResult(Init)
 
      syntax KItem ::= declareNonStaticObject2(K, Bool)
 
diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k
index a4e29abcb..05a61e832 100644
--- a/semantics/cpp/language/translation/decl/initializer.k
+++ b/semantics/cpp/language/translation/decl/initializer.k
@@ -86,7 +86,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
           requires notBool isSpuriousExpr(HOLE) [result(ValueCategory)]
 
      rule <k> #figureInit(Base::Expr, DestT::CPPType, IType::InitType,
-               I::Init, SrcType::CPPType, SrcCat::ValueCategory,
+               I::Init, SrcType::K, SrcCat::K,
                CT::ConstructorType, D::Duration)
           =>
           Base ~> #figureInitHeatBase(DestT, IType, I, SrcType, SrcCat, CT, D)
@@ -95,7 +95,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
           requires notBool isLVal(Base)
 
      rule <k> Base:LVal ~> #figureInitHeatBase(DestT::CPPType, IType::InitType,
-               I::Init, SrcType::CPPType, SrcCat::ValueCategory,
+               I::Init, SrcType::K, SrcCat::K,
                CT::ConstructorType, D::Duration)
           =>
           #figureInit(Base, DestT, IType, I, SrcType, SrcCat, CT, D)
@@ -329,13 +329,13 @@ module CPP-TRANSLATION-DECL-INITIALIZER
 
      syntax Bool ::= hasInit(CId, Map) [function]
 
-     rule hasInit(X:CId, X |-> M::Map _) => notBool isNoInit(M)
+     rule hasInit(X:CId, X |-> M::Map _) => notBool hasNoInit(M)
 
-     syntax Bool ::= isNoInit(Map) [function]
+     syntax Bool ::= hasNoInit(Map) [function]
 
-     rule isNoInit(_ |-> (_, NoInit())) => true
+     rule hasNoInit(_ |-> (_, NoInit())) => true
 
-     rule isNoInit(_ |-> _) => false [owise]
+     rule hasNoInit(_ |-> _) => false [owise]
 
      syntax Expr ::= classAggInit(base: LVal, fields: List, initList: List, initializers: Map, class: Class, initExp: K, ctype: ConstructorType, duration: Duration)
 
@@ -409,7 +409,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
        ~> classAggInit(... base: Base::LVal,
                            fields: (ListItem(Class.DataMember(F:CId, _)) => .List) _,
                            initList: .List,
-                           initializers: (F |-> (_::CPPType |-> (T::CPPType, Init::Expr))) _,
+                           initializers: (F |-> (_::CPPType |-> (T::CPPType, Init::Init))) _,
                            class: C::Class,
                            duration: D::Duration)
 
diff --git a/semantics/cpp/language/translation/env.k b/semantics/cpp/language/translation/env.k
index 14d82cc72..06eaae10e 100644
--- a/semantics/cpp/language/translation/env.k
+++ b/semantics/cpp/language/translation/env.k
@@ -17,7 +17,7 @@ module CPP-TRANSLATION-ENV-SYNTAX
 
      syntax KItem ::= "pushLocals" | "popLocals"
 
-     syntax KItem ::= updateDefaultArguments(QualId, CPPType, DefaultArguments) [strict(3)]
+     syntax KItem ::= updateDefaultArguments(QualId, CPPType, DefaultArguments)
 
      syntax List ::= getDefaultArgsVals(DefaultArgumentsResult) [function]
 
@@ -42,6 +42,11 @@ module CPP-TRANSLATION-ENV
     rule updateDefaultArguments(_, T::CPPType, _) => .K
          requires notBool isCPPFunctionType(T)
 
+     // if T is not a function type, the HOLE evaluates to `krlist`,
+     // which is not of sort `DefaultArguments`
+     context updateDefaultArguments(_, T::CPPType, HOLE:DefaultArguments)
+          requires isCPPFunctionType(T)
+
     rule <k> addToEnv(N:Namespace :: X::CId, t(... st: functionType(...)) #as T::CPPType, Base::SymBase, IsUsing::Bool)
              => .K
          ...</k>
diff --git a/semantics/cpp/language/translation/name.k b/semantics/cpp/language/translation/name.k
index 54893f216..8c9434fbd 100644
--- a/semantics/cpp/language/translation/name.k
+++ b/semantics/cpp/language/translation/name.k
@@ -263,7 +263,7 @@ module CPP-TRANSLATION-NAME
           <enumerators>... X |-> V::PRVal </enumerators>
           requires variable in Mask
 
-     rule <k> lookupEnumerator(X::CId, E::Enum, Mask::Set, C:K) => #if C ==K .K #then prv(V, Tr, ET) #else classSet(prv(V, Tr, ET), {C}:>Class :: X, SetItem({C}:>Class)) #fi ... </k>
+     rule <k> lookupEnumerator(X::CId, E::Enum, Mask::Set, C:K) => #if C ==K .K #then {prv(V, Tr, ET)}:>KItem #else {classSet(prv(V, Tr, ET), {C}:>Class :: X, SetItem({C}:>Class))}:>KItem #fi ... </k>
           <curr-tr-scope> Sc::Scope </curr-tr-scope>
           <enum-id> E </enum-id>
           <enum-type> ET::CPPType </enum-type>
diff --git a/semantics/cpp/language/translation/overloading.k b/semantics/cpp/language/translation/overloading.k
index c7b926cb2..8c75e4872 100644
--- a/semantics/cpp/language/translation/overloading.k
+++ b/semantics/cpp/language/translation/overloading.k
@@ -124,9 +124,9 @@ module CPP-TRANSLATION-OVERLOADING
      rule getArgs(Args::List, _, constructor, _) => Args
 
      // strict version
-     rule cSetUnion(notFound(_), E::Expr) => E
+     rule cSetUnion(notFound(_), E::KItem) => E
 
-     rule cSetUnion(E::Expr, notFound(_)) => E
+     rule cSetUnion(E::KItem, notFound(_)) => E
 
      rule cSetUnion(cSet(M1::Map, QX::QualId), cSet(M2::Map, QX)) => cSet(M1 M2, QX)
 
@@ -1099,8 +1099,8 @@ module CPP-TRANSLATION-OVERLOADING
           #fi
           requires isCPPRefType(T)
 
-     rule resolveUniqueDecl(V:KResult, _, _) => V
-          requires notBool isCandidateSet(V) andBool notBool isNotFoundNameRef(V)
+     rule resolveUniqueDecl(V:KItem, _, _) => V
+          requires isKResult(V) andBool notBool isCandidateSet(V) andBool notBool isNotFoundNameRef(V)
 
      rule (.K => ILL("TOL1", "No declaration found for name '" +String showCId(X) +String "'.")) ~> resolveUniqueDecl(notFound(X::CId), _, _)
 
diff --git a/semantics/cpp/language/translation/process-label.k b/semantics/cpp/language/translation/process-label.k
index 5d46ce5cd..e80f86581 100644
--- a/semantics/cpp/language/translation/process-label.k
+++ b/semantics/cpp/language/translation/process-label.k
@@ -106,7 +106,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <goto-calc>
                <computation>
-                    (ForStmt(Control:Expr, Post::Stmt, S::Stmt) => .K)
+                    (ForStmt(Control:Expr, Post::K, S::K) => .K)
                     ~> K:K
                </computation>
                <computation-tail> Tail:K </computation-tail>
@@ -141,7 +141,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <computation>
                (.K => S ~> loopMarked)
-               ~> WhileStmt(_:Expr, S::Stmt)
+               ~> WhileStmt(_:Expr, S::K)
                ~> (.K => popLoop)
                ~> K:K
           </computation>
@@ -159,7 +159,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <goto-calc>
                <computation>
-                    (IfStmt(_:Expr, S1::Block, S2::Block) => .K) ~> K:K
+                    (IfStmt(_:Expr, S1::K, S2::K) => .K) ~> K:K
                </computation>
                <computation-tail> Tail:K </computation-tail>
                B::Bag
@@ -182,7 +182,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <goto-calc>
                <computation>
-                    (TryStmt(S::Block, .List) => .K) ~> K:K
+                    (TryStmt(S::K, .List) => .K) ~> K:K
                </computation>
                <computation-tail> Tail:K </computation-tail>
                B::Bag
@@ -196,7 +196,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <goto-calc>
                <computation>
-                    TryStmt(_, (ListItem(CatchOp(T::CPPType, S::Block)) => .List) L::List) ~> K:K
+                    TryStmt(_, (ListItem(CatchOp(T::CPPType, S::K)) => .List) L::List) ~> K:K
                </computation>
                <computation-tail> Tail:K </computation-tail>
                B::Bag
@@ -210,7 +210,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <goto-calc>
                <computation>
-                    TryStmt(_, (ListItem(CatchAnyOp(S::Block)) => .List) L::List) ~> K:K
+                    TryStmt(_, (ListItem(CatchAnyOp(S::K)) => .List) L::List) ~> K:K
                </computation>
                <computation-tail> Tail:K </computation-tail>
                B::Bag
diff --git a/semantics/cpp/language/translation/stmt/canonicalization.k b/semantics/cpp/language/translation/stmt/canonicalization.k
index 731901267..6aa7f4bcb 100644
--- a/semantics/cpp/language/translation/stmt/canonicalization.k
+++ b/semantics/cpp/language/translation/stmt/canonicalization.k
@@ -44,7 +44,7 @@ module CPP-TRANSLATION-STMT-CANONICALIZATION
 
       rule canonicalizeAStmts(ListItem(E:Expr) L::List) => ListItem(TExpressionStmt(E)) canonicalizeAStmts(L)
 
-      rule canonicalizeAStmts(ListItem(S::Stmt) L::List) => ListItem(S) canonicalizeAStmts(L) [owise]
+      rule canonicalizeAStmts(ListItem(S:AStmt) L::List) => ListItem(S) canonicalizeAStmts(L) [owise]
 
       rule canonicalizeAStmts(.List) => .List
 
diff --git a/semantics/cpp/language/translation/stmt/try.k b/semantics/cpp/language/translation/stmt/try.k
index 06f88dead..7e9bde1d9 100644
--- a/semantics/cpp/language/translation/stmt/try.k
+++ b/semantics/cpp/language/translation/stmt/try.k
@@ -98,6 +98,6 @@ module CPP-TRANSLATION-STMT-TRY
 
      rule processCatchDecl(NormalizedDecl(... type: t(... st: functionType(...)) #as T::CPPType => type(pointerType(T))))
 
-     rule processCatchDecl(D::Decl) => D [owise]
+     rule processCatchDecl(D::Declarator) => D [owise]
 
 endmodule
diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k
index a61bd8756..9bdcaac81 100644
--- a/semantics/cpp/language/translation/syntax.k
+++ b/semantics/cpp/language/translation/syntax.k
@@ -49,9 +49,9 @@ module CPP-ABSTRACT-SYNTAX
                       | ConstructorMember(CId, Init) [symbol]
                       | ConstructorDelegating(Init) [symbol]
 
-     syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, AStmt) [strict(4), symbol]
-                         | FunctionDecl(NNS, CId, CId, AType, List) [strict(4), symbol]
-                         | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [strict(4), symbol]
+     syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, AStmt) [symbol]
+                         | FunctionDecl(NNS, CId, CId, AType, List) [symbol]
+                         | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [symbol]
                          | FieldDecl(NNS, CId, AType, Init) [strict(3), symbol]
                          | BitFieldDecl(NNS, CId, AType, Expr) [strict(3), symbol]
 
@@ -99,6 +99,8 @@ module CPP-ABSTRACT-SYNTAX
 
      syntax Enumerator ::= Enumerator(CId, AExpr) [symbol]
 
+     syntax Decl ::= Enumerator
+
      syntax CPPType // defined in CPP-TYPING-SYNTAX
 
      syntax ATypeResult ::= NoType() [symbol]
@@ -191,7 +193,7 @@ module CPP-ABSTRACT-SYNTAX
                    | ForTStmt(Stmt, Decl, Stmt, Stmt)
                    | ForTStmt(Expr, Stmt, Stmt)
                    | TemplateDefinitionStmt(K) [symbol] // synthetic statement created by the body of a function template definition when it's evaluted before instantiation
-                   | TReturnOp(init: Expr, obj: K)
+                   | TReturnOp(init: Expr, obj: K) [symbol]
 
      syntax AStmt ::= NoStatement() [symbol]
                     | CompoundAStmt(List) [symbol]
@@ -201,10 +203,10 @@ module CPP-ABSTRACT-SYNTAX
                     | WhileAStmt(Decl, AStmt)
                     | WhileAStmt(Expr, AStmt) [symbol]
                     | DoWhileAStmt(AStmt, Expr) [symbol]
-                    | IfAStmt(Decl, AStmt, AStmt) [symbol]
-                    | IfAStmt(Expr, AStmt, AStmt)
-                    | SwitchAStmt(Decl, AStmt) [symbol]
-                    | SwitchAStmt(Expr, AStmt)
+                    | IfAStmtD(Decl, AStmt, AStmt) [symbol]
+                    | IfAStmt(Expr, AStmt, AStmt) [symbol]
+                    | SwitchAStmtD(Decl, AStmt) [symbol]
+                    | SwitchAStmt(Expr, AStmt) [symbol]
                     | CaseAStmt(Expr, AStmt) [symbol]
                     | DefaultAStmt(AStmt) [symbol]
                     | TryAStmt(AStmt, List) [symbol]
@@ -214,7 +216,7 @@ module CPP-ABSTRACT-SYNTAX
 
      syntax Stmt ::= Defaulted() [symbol]
                     | Deleted() [symbol]
-                    | Constructor(List, Stmt) [symbol]
+                    | Constructor(List, AStmt) [symbol]
                     | Destructor() [symbol]
 
      syntax CatchDecl ::= Decl | Ellipsis() [symbol]
diff --git a/semantics/linking/configuration.k b/semantics/linking/configuration.k
index 339871e99..c8df194ea 100644
--- a/semantics/linking/configuration.k
+++ b/semantics/linking/configuration.k
@@ -17,7 +17,7 @@ module C-CONFIGURATION
 
 <exec>
      <k color="green">
-          load($OBJS:K)
+          $OBJS:KItem
           ~> linkProgram(getEntryPoint($OPTIONS:Set))
           ~> cleanup
      </k>
diff --git a/semantics/linking/cpp-resolution.k b/semantics/linking/cpp-resolution.k
index b898e27ab..ae4c28558 100644
--- a/semantics/linking/cpp-resolution.k
+++ b/semantics/linking/cpp-resolution.k
@@ -45,7 +45,9 @@ module LINKING-CPP-RESOLUTION
           <tu-id> Tu </tu-id>
           <ns-id> N </ns-id>
           <nenv>... X |-> (stripType(T) |-> (_, envEntry(... base: Base::SymBase => Base')) _::Map) ...</nenv>
-          <linkings>... .Map => Base |-> Base' ...</linkings>
+          <linkings> Linkings::Map => Linkings[Base <- Base'] </linkings>
+          // do not overwrite the old value with a different one
+          requires (Linkings[Base] orDefault Base') ==K Base'
 
      rule <k> resolveCPPReference(OdrBase::SymBase) ...</k>
           <odr-decls>...
diff --git a/semantics/linking/init.k b/semantics/linking/init.k
index e55cf62be..e1b1b3abe 100644
--- a/semantics/linking/init.k
+++ b/semantics/linking/init.k
@@ -371,4 +371,9 @@ module LINKING-INIT
      syntax Map ::= getOverridden(Map, Map) [function]
      rule getOverridden(_, _) => .Map::Map [owise]
 
+     rule hasTrace(_) => noTrace [anywhere]
+
+     rule <initializers> M => .Map </initializers>
+          requires M =/=K .Map [anywhere]
+
 endmodule