diff --git a/docs/proof-trace.md b/docs/proof-trace.md
index 1b700a9b0..f034c45fd 100644
--- a/docs/proof-trace.md
+++ b/docs/proof-trace.md
@@ -54,13 +54,13 @@ hook              ::= WORD(0xAA) name symbol_name location arg* WORD(0xBB) kore_
 ordinal           ::= uint64
 arity             ::= uint64
 boolean_result    ::= uint8
-variable          ::= name kore_term WORD(0xCC)
+variable          ::= name kore_term
 rule              ::= WORD(0x22) ordinal arity variable*
 
 side_cond_entry   ::= WORD(0xEE) ordinal arity variable*
 side_cond_exit    ::= WORD(0x33) ordinal boolean_result
 
-config            ::= WORD(0xFF) kore_term WORD(0xCC)
+config            ::= WORD(0xFF) kore_term
 
 string            ::= <c-style null terminated string>
 uint64            ::= <64-bit unsigned little endian integer>
diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h
index 828e23c5a..57139b6c3 100644
--- a/include/kllvm/binary/ProofTraceParser.h
+++ b/include/kllvm/binary/ProofTraceParser.h
@@ -26,7 +26,6 @@ static_assert(word(0xAA) == 0xAAAAAAAAAAAAAAAA);
 } // namespace detail
 
 constexpr uint64_t config_sentinel = detail::word(0xFF);
-constexpr uint64_t kore_end_sentinel = detail::word(0xCC);
 constexpr uint64_t function_event_sentinel = detail::word(0xDD);
 constexpr uint64_t function_end_sentinel = detail::word(0x11);
 constexpr uint64_t hook_event_sentinel = detail::word(0xAA);
@@ -274,7 +273,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 10U;
+  static constexpr uint32_t expected_version = 11U;
 
 private:
   bool verbose_;
@@ -332,7 +331,7 @@ class proof_trace_parser {
 
     event->add_substitution(name, kore_term, pattern_len);
 
-    return buffer.check_word(kore_end_sentinel);
+    return true;
   }
 
   sptr<llvm_hook_event> parse_hook(proof_trace_buffer &buffer) {
@@ -422,10 +421,6 @@ class proof_trace_parser {
       return nullptr;
     }
 
-    if (!buffer.check_word(kore_end_sentinel)) {
-      return nullptr;
-    }
-
     return kore_term;
   }
 
diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp
index 455896123..303fd6e61 100644
--- a/lib/codegen/ProofEvent.cpp
+++ b/lib/codegen/ProofEvent.cpp
@@ -255,7 +255,6 @@ llvm::BasicBlock *proof_event::rewrite_event_pre(
 
     emit_write_string(outputFile, key.str(), true_block);
     emit_serialize_term(*sort, outputFile, val, true_block);
-    emit_write_uint64(outputFile, detail::word(0xCC), true_block);
   }
 
   llvm::BranchInst::Create(merge_block, true_block);
@@ -277,7 +276,6 @@ llvm::BasicBlock *proof_event::rewrite_event_post(
 
   emit_write_uint64(output_file, detail::word(0xFF), true_block);
   emit_serialize_term(*return_sort, output_file, return_value, true_block);
-  emit_write_uint64(output_file, detail::word(0xCC), true_block);
 
   llvm::BranchInst::Create(merge_block, true_block);
   return merge_block;
@@ -353,7 +351,6 @@ llvm::BasicBlock *proof_event::side_condition_event_pre(
 
     emit_write_string(outputFile, var_name, true_block);
     emit_serialize_term(*sort, outputFile, val, true_block);
-    emit_write_uint64(outputFile, detail::word(0xCC), true_block);
   }
 
   llvm::BranchInst::Create(merge_block, true_block);
diff --git a/runtime/take_steps.ll b/runtime/take_steps.ll
index 06f6c338a..fb5cdffd2 100644
--- a/runtime/take_steps.ll
+++ b/runtime/take_steps.ll
@@ -52,7 +52,6 @@ if:
   %output_file = load i8*, i8** @output_file
   call void @write_uint64_to_file(i8* %output_file, i64 18446744073709551615)
   call void @serialize_configuration_to_file_v2(i8* %output_file, %block* %subject)
-  call void @write_uint64_to_file(i8* %output_file, i64 14757395258967641292)
   br label %merge
 merge:
   store i64 %depth, i64* @depth
diff --git a/runtime/util/finish_rewriting.cpp b/runtime/util/finish_rewriting.cpp
index 3a27bc60f..1e57dc462 100644
--- a/runtime/util/finish_rewriting.cpp
+++ b/runtime/util/finish_rewriting.cpp
@@ -48,7 +48,6 @@ int32_t get_exit_code(block *);
   } else if (!error && !proof_hint_instrumentation_slow) {
     write_uint64_to_file(output_file, 0xFFFFFFFFFFFFFFFF);
     serialize_configuration_to_file_v2(output_file, subject);
-    write_uint64_to_file(output_file, 0xCCCCCCCCCCCCCCCC);
   }
 
   auto exit_code = error ? 113 : get_exit_code(subject);
diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp
index 3a9fe9e59..de5a196c4 100644
--- a/runtime/util/util.cpp
+++ b/runtime/util/util.cpp
@@ -35,7 +35,7 @@ block *construct_raw_term(void *subject, char const *sort, bool raw_value) {
 }
 
 void print_proof_hint_header(FILE *file) {
-  uint32_t version = 10;
+  uint32_t version = 11;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }
diff --git a/test/output/add-rewrite/input.proof.out.diff b/test/output/add-rewrite/input.proof.out.diff
index 6d10fcebb..a49474416 100644
--- a/test/output/add-rewrite/input.proof.out.diff
+++ b/test/output/add-rewrite/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/arith/add.proof.out.diff b/test/output/arith/add.proof.out.diff
index 78c899638..d3cca85d4 100644
--- a/test/output/arith/add.proof.out.diff
+++ b/test/output/arith/add.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/arith/well.proof.out.diff b/test/output/arith/well.proof.out.diff
index 0eaeff5e2..a4d7bad10 100644
--- a/test/output/arith/well.proof.out.diff
+++ b/test/output/arith/well.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/assoc-function/left.proof.out.diff b/test/output/assoc-function/left.proof.out.diff
index d36bcc79f..2c03d9b5a 100644
--- a/test/output/assoc-function/left.proof.out.diff
+++ b/test/output/assoc-function/left.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{} ()
 rule: 103 2
   Var'Unds'X = kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
diff --git a/test/output/assoc-function/next-left.proof.out.diff b/test/output/assoc-function/next-left.proof.out.diff
index 19a01dda6..70051e60a 100644
--- a/test/output/assoc-function/next-left.proof.out.diff
+++ b/test/output/assoc-function/next-left.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{} ()
 rule: 103 2
   Var'Unds'X = kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
diff --git a/test/output/assoc-function/next-right.proof.out.diff b/test/output/assoc-function/next-right.proof.out.diff
index ff70fd68c..5a42b1350 100644
--- a/test/output/assoc-function/next-right.proof.out.diff
+++ b/test/output/assoc-function/next-right.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{} ()
 rule: 104 2
   Var'Unds'Y = kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
diff --git a/test/output/assoc-function/right.proof.out.diff b/test/output/assoc-function/right.proof.out.diff
index 7cf524f0d..1fcd704bc 100644
--- a/test/output/assoc-function/right.proof.out.diff
+++ b/test/output/assoc-function/right.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{} ()
 rule: 104 2
   Var'Unds'Y = kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
diff --git a/test/output/builtin-functions/abs.proof.out.diff b/test/output/builtin-functions/abs.proof.out.diff
index abc7cf011..f9973e176 100644
--- a/test/output/builtin-functions/abs.proof.out.diff
+++ b/test/output/builtin-functions/abs.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblabs'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Int'Unds'Int{} ()
 rule: 210 1
   VarI = kore[\dv{SortInt{}}("-5")]
diff --git a/test/output/builtin-functions/double.proof.out.diff b/test/output/builtin-functions/double.proof.out.diff
index 82c0be0f3..575999e86 100644
--- a/test/output/builtin-functions/double.proof.out.diff
+++ b/test/output/builtin-functions/double.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbldouble'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Int'Unds'Int{} ()
 rule: 214 1
   VarI = kore[\dv{SortInt{}}("5")]
diff --git a/test/output/builtin-functions/head-bytes.proof.out.diff b/test/output/builtin-functions/head-bytes.proof.out.diff
index 87c2631e0..066640797 100644
--- a/test/output/builtin-functions/head-bytes.proof.out.diff
+++ b/test/output/builtin-functions/head-bytes.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblhead'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Bytes'Unds'Bytes{} ()
 rule: 219 1
   VarB = kore[\dv{SortBytes{}}("bytes")]
diff --git a/test/output/builtin-functions/head-string.proof.out.diff b/test/output/builtin-functions/head-string.proof.out.diff
index 35ea9c99e..9e2b7b9be 100644
--- a/test/output/builtin-functions/head-string.proof.out.diff
+++ b/test/output/builtin-functions/head-string.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblhead'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'String'Unds'String{} ()
 rule: 220 1
   VarS = kore[\dv{SortString{}}("string")]
diff --git a/test/output/builtin-functions/ispos.proof.out.diff b/test/output/builtin-functions/ispos.proof.out.diff
index 036c591bc..bfd6c5066 100644
--- a/test/output/builtin-functions/ispos.proof.out.diff
+++ b/test/output/builtin-functions/ispos.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: LblisPos'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Bool'Unds'Int{} ()
 rule: 255 1
   VarI = kore[\dv{SortInt{}}("0")]
diff --git a/test/output/builtin-functions/next-abs.proof.out.diff b/test/output/builtin-functions/next-abs.proof.out.diff
index 1fb9322ad..9235e98de 100644
--- a/test/output/builtin-functions/next-abs.proof.out.diff
+++ b/test/output/builtin-functions/next-abs.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblabs'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Int'Unds'Int{} ()
 rule: 210 1
   VarI = kore[\dv{SortInt{}}("-5")]
diff --git a/test/output/builtin-functions/next-double.proof.out.diff b/test/output/builtin-functions/next-double.proof.out.diff
index d321eedc4..a2b0229de 100644
--- a/test/output/builtin-functions/next-double.proof.out.diff
+++ b/test/output/builtin-functions/next-double.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbldouble'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Int'Unds'Int{} ()
 rule: 214 1
   VarI = kore[\dv{SortInt{}}("5")]
diff --git a/test/output/builtin-functions/next-head-bytes.proof.out.diff b/test/output/builtin-functions/next-head-bytes.proof.out.diff
index 3b79ac7cb..3f7789fbb 100644
--- a/test/output/builtin-functions/next-head-bytes.proof.out.diff
+++ b/test/output/builtin-functions/next-head-bytes.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblhead'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Bytes'Unds'Bytes{} ()
 rule: 219 1
   VarB = kore[\dv{SortBytes{}}("bytes")]
diff --git a/test/output/builtin-functions/next-head-string.proof.out.diff b/test/output/builtin-functions/next-head-string.proof.out.diff
index 71b4fcfeb..1c5e53f06 100644
--- a/test/output/builtin-functions/next-head-string.proof.out.diff
+++ b/test/output/builtin-functions/next-head-string.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblhead'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'String'Unds'String{} ()
 rule: 220 1
   VarS = kore[\dv{SortString{}}("string")]
diff --git a/test/output/builtin-functions/next-ispos.proof.out.diff b/test/output/builtin-functions/next-ispos.proof.out.diff
index e6d8c0257..23436e014 100644
--- a/test/output/builtin-functions/next-ispos.proof.out.diff
+++ b/test/output/builtin-functions/next-ispos.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: LblisPos'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Bool'Unds'Int{} ()
 rule: 255 1
   VarI = kore[\dv{SortInt{}}("0")]
diff --git a/test/output/builtin-hook-events/program.proof.out.diff b/test/output/builtin-hook-events/program.proof.out.diff
index 48e5a25f7..93a9f8c77 100644
--- a/test/output/builtin-hook-events/program.proof.out.diff
+++ b/test/output/builtin-hook-events/program.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/builtin-int/input.proof.out.diff b/test/output/builtin-int/input.proof.out.diff
index a96578257..cee5d3d1e 100644
--- a/test/output/builtin-int/input.proof.out.diff
+++ b/test/output/builtin-int/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/builtin-io/read.proof.out.diff b/test/output/builtin-io/read.proof.out.diff
index b6ab4c0db..4d4fa4a09 100644
--- a/test/output/builtin-io/read.proof.out.diff
+++ b/test/output/builtin-io/read.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/builtin-json/id.proof.out.diff b/test/output/builtin-json/id.proof.out.diff
index 8686c253a..964e8d005 100644
--- a/test/output/builtin-json/id.proof.out.diff
+++ b/test/output/builtin-json/id.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblid'LParUndsRParUnds'BUILTIN-JSON-SYNTAX'Unds'JSON'Unds'JSON{} ()
 rule: 216 1
   VarJ = kore[LblJSONObject{}(LblJSONs{}(LblJSONEntry{}(\dv{SortString{}}("key"),\dv{SortInt{}}("2")),Lbl'Stop'List'LBraQuot'JSONs'QuotRBra'{}()))]
diff --git a/test/output/builtin-json/next-id.proof.out.diff b/test/output/builtin-json/next-id.proof.out.diff
index 39344844b..23eded8de 100644
--- a/test/output/builtin-json/next-id.proof.out.diff
+++ b/test/output/builtin-json/next-id.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblid'LParUndsRParUnds'BUILTIN-JSON-SYNTAX'Unds'JSON'Unds'JSON{} ()
 rule: 216 1
   VarJ = kore[LblJSONObject{}(LblJSONs{}(LblJSONEntry{}(\dv{SortString{}}("key"),\dv{SortInt{}}("2")),Lbl'Stop'List'LBraQuot'JSONs'QuotRBra'{}()))]
diff --git a/test/output/cast/in.proof.out.diff b/test/output/cast/in.proof.out.diff
index cd5238b45..c5a88f68a 100644
--- a/test/output/cast/in.proof.out.diff
+++ b/test/output/cast/in.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/cell-collection/exec.proof.out.diff b/test/output/cell-collection/exec.proof.out.diff
index 46d2dc699..0fa1b9eb9 100644
--- a/test/output/cell-collection/exec.proof.out.diff
+++ b/test/output/cell-collection/exec.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/cell-value/init.proof.out.diff b/test/output/cell-value/init.proof.out.diff
index f9728ac72..c98105f92 100644
--- a/test/output/cell-value/init.proof.out.diff
+++ b/test/output/cell-value/init.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/concurrent-counters/4.proof.out.diff b/test/output/concurrent-counters/4.proof.out.diff
index 4cbbb86e5..0a046701c 100644
--- a/test/output/concurrent-counters/4.proof.out.diff
+++ b/test/output/concurrent-counters/4.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/conditional-function/3.proof.out.diff b/test/output/conditional-function/3.proof.out.diff
index f15537343..9a54ae7e3 100644
--- a/test/output/conditional-function/3.proof.out.diff
+++ b/test/output/conditional-function/3.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/custom-klabel-fun/input.proof.out.diff b/test/output/custom-klabel-fun/input.proof.out.diff
index 649bc8650..37dd0d00a 100644
--- a/test/output/custom-klabel-fun/input.proof.out.diff
+++ b/test/output/custom-klabel-fun/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblbar1'LParUndsRParUnds'CUSTOM-KLABEL-FUN-SYNTAX'Unds'Foo'Unds'Foo{} ()
 rule: 92 1
   VarX = kore[Lbla'Unds'CUSTOM-KLABEL-FUN-SYNTAX'Unds'Foo{}()]
diff --git a/test/output/decrement-int/2_rewrites.proof.out.diff b/test/output/decrement-int/2_rewrites.proof.out.diff
index 2ab0f1026..aabc4a988 100644
--- a/test/output/decrement-int/2_rewrites.proof.out.diff
+++ b/test/output/decrement-int/2_rewrites.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/decrement/0_rewrites.proof.out.diff b/test/output/decrement/0_rewrites.proof.out.diff
index a0a59dbaf..f49ef3231 100644
--- a/test/output/decrement/0_rewrites.proof.out.diff
+++ b/test/output/decrement/0_rewrites.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/decrement/1_rewrite.proof.out.diff b/test/output/decrement/1_rewrite.proof.out.diff
index 701b888af..a232d9b7c 100644
--- a/test/output/decrement/1_rewrite.proof.out.diff
+++ b/test/output/decrement/1_rewrite.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/decrement/2_rewrites.proof.out.diff b/test/output/decrement/2_rewrites.proof.out.diff
index f39f6516b..04780b878 100644
--- a/test/output/decrement/2_rewrites.proof.out.diff
+++ b/test/output/decrement/2_rewrites.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/double-rewrite/foo-a.proof.out.diff b/test/output/double-rewrite/foo-a.proof.out.diff
index 55344e25b..b41f1cc4b 100644
--- a/test/output/double-rewrite/foo-a.proof.out.diff
+++ b/test/output/double-rewrite/foo-a.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/dv/five.proof.out.diff b/test/output/dv/five.proof.out.diff
index ddcb08d09..1184fb1de 100644
--- a/test/output/dv/five.proof.out.diff
+++ b/test/output/dv/five.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/exit-cell/exec0.output-cell.proof.out.diff b/test/output/exit-cell/exec0.output-cell.proof.out.diff
index 0d529fb48..f5120136e 100644
--- a/test/output/exit-cell/exec0.output-cell.proof.out.diff
+++ b/test/output/exit-cell/exec0.output-cell.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/fresh-gen/init.proof.out.diff b/test/output/fresh-gen/init.proof.out.diff
index a5828b883..5faa71274 100644
--- a/test/output/fresh-gen/init.proof.out.diff
+++ b/test/output/fresh-gen/init.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/fun-context/exec.proof.out.diff b/test/output/fun-context/exec.proof.out.diff
index 61ff0f909..52e354bd3 100644
--- a/test/output/fun-context/exec.proof.out.diff
+++ b/test/output/fun-context/exec.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp-sum-slow.proof.out.diff b/test/output/imp-sum-slow.proof.out.diff
index 83b0bb634..dfbdd49e4 100644
--- a/test/output/imp-sum-slow.proof.out.diff
+++ b/test/output/imp-sum-slow.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
     arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp-sum.proof.out.diff b/test/output/imp-sum.proof.out.diff
index a66dc0735..35b77b501 100644
--- a/test/output/imp-sum.proof.out.diff
+++ b/test/output/imp-sum.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp.proof.out.diff b/test/output/imp.proof.out.diff
index af991d048..d1bca007d 100644
--- a/test/output/imp.proof.out.diff
+++ b/test/output/imp.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$IO")]
diff --git a/test/output/imp/empty.proof.out.diff b/test/output/imp/empty.proof.out.diff
index 773804f8a..aac050d4c 100644
--- a/test/output/imp/empty.proof.out.diff
+++ b/test/output/imp/empty.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp5-rw-literal/empty.proof.out.diff b/test/output/imp5-rw-literal/empty.proof.out.diff
index e9daa42c0..b432e6c53 100644
--- a/test/output/imp5-rw-literal/empty.proof.out.diff
+++ b/test/output/imp5-rw-literal/empty.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp5-rw-literal/transfer.proof.out.diff b/test/output/imp5-rw-literal/transfer.proof.out.diff
index e3b9f645c..a62aa3a01 100644
--- a/test/output/imp5-rw-literal/transfer.proof.out.diff
+++ b/test/output/imp5-rw-literal/transfer.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp5-rw-succ/empty.proof.out.diff b/test/output/imp5-rw-succ/empty.proof.out.diff
index 042faa0e9..e8f15682e 100644
--- a/test/output/imp5-rw-succ/empty.proof.out.diff
+++ b/test/output/imp5-rw-succ/empty.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp5-rw-succ/transfer.proof.out.diff b/test/output/imp5-rw-succ/transfer.proof.out.diff
index c54655bcb..029c9e4c8 100644
--- a/test/output/imp5-rw-succ/transfer.proof.out.diff
+++ b/test/output/imp5-rw-succ/transfer.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp5/empty.proof.out.diff b/test/output/imp5/empty.proof.out.diff
index cf5dcac9f..c58d90b50 100644
--- a/test/output/imp5/empty.proof.out.diff
+++ b/test/output/imp5/empty.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/imp5/transfer.proof.out.diff b/test/output/imp5/transfer.proof.out.diff
index 1be4f966e..dae1c728f 100644
--- a/test/output/imp5/transfer.proof.out.diff
+++ b/test/output/imp5/transfer.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/injections/input.proof.out.diff b/test/output/injections/input.proof.out.diff
index 05b740838..13ccd8bad 100644
--- a/test/output/injections/input.proof.out.diff
+++ b/test/output/injections/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/is-zero/zero.proof.out.diff b/test/output/is-zero/zero.proof.out.diff
index 2d9c4729c..13f10a419 100644
--- a/test/output/is-zero/zero.proof.out.diff
+++ b/test/output/is-zero/zero.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: LblisZero'LParUndsRParUnds'IS-ZERO-SYNTAX'Unds'Bool'Unds'Int{} ()
 rule: 181 0
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
diff --git a/test/output/kool-static.proof.out.diff b/test/output/kool-static.proof.out.diff
index 0ed3b87fd..c7c6d7910 100644
--- a/test/output/kool-static.proof.out.diff
+++ b/test/output/kool-static.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$IO")]
diff --git a/test/output/lambda-explicit-subst/in1.proof.out.diff b/test/output/lambda-explicit-subst/in1.proof.out.diff
index 0d9eee7d5..69ded405e 100644
--- a/test/output/lambda-explicit-subst/in1.proof.out.diff
+++ b/test/output/lambda-explicit-subst/in1.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/lambda-explicit-subst/in2.proof.out.diff b/test/output/lambda-explicit-subst/in2.proof.out.diff
index d4e17d1cc..b94725c05 100644
--- a/test/output/lambda-explicit-subst/in2.proof.out.diff
+++ b/test/output/lambda-explicit-subst/in2.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/lambda-explicit-subst/in3.proof.out.diff b/test/output/lambda-explicit-subst/in3.proof.out.diff
index cc8543963..21ed0ad57 100644
--- a/test/output/lambda-explicit-subst/in3.proof.out.diff
+++ b/test/output/lambda-explicit-subst/in3.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/let/foo.proof.out.diff b/test/output/let/foo.proof.out.diff
index e3d0c73cc..92b0d7e03 100644
--- a/test/output/let/foo.proof.out.diff
+++ b/test/output/let/foo.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblexp'LParUndsRParUnds'LET-SYNTAX'Unds'Int'Unds'Int{} ()
 rule: 151 1
   VarX = kore[\dv{SortInt{}}("10")]
diff --git a/test/output/list-assoc/input.proof.out.diff b/test/output/list-assoc/input.proof.out.diff
index 683cbab99..a51e8935e 100644
--- a/test/output/list-assoc/input.proof.out.diff
+++ b/test/output/list-assoc/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'Hash'revOps'LParUndsRParUnds'LIST-ASSOC-SYNTAX'Unds'OpCodes'Unds'OpCodes{} ()
 rule: 102 1
   VarOPS = kore[Lbl'UndsSClnUndsUnds'LIST-ASSOC-SYNTAX'Unds'OpCodes'Unds'OpCodes'Unds'OpCodes{}(Lblload'Unds'LIST-ASSOC-SYNTAX'Unds'OpCode{}(),Lbl'UndsSClnUndsUnds'LIST-ASSOC-SYNTAX'Unds'OpCodes'Unds'OpCodes'Unds'OpCodes{}(Lblstore'Unds'LIST-ASSOC-SYNTAX'Unds'OpCode{}(),LblnoOp'Unds'LIST-ASSOC-SYNTAX'Unds'OpCode{}()))]
diff --git a/test/output/list-cons/input.proof.out.diff b/test/output/list-cons/input.proof.out.diff
index 542e1f43e..37ae643e1 100644
--- a/test/output/list-cons/input.proof.out.diff
+++ b/test/output/list-cons/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'Hash'revOps'LParUndsRParUnds'LIST-CONS-SYNTAX'Unds'OpCodes'Unds'OpCodes{} ()
 rule: 103 1
   VarOPS = kore[Lbl'UndsSClnUndsUnds'LIST-CONS-SYNTAX'Unds'OpCodes'Unds'OpCode'Unds'OpCodes{}(Lblload'Unds'LIST-CONS-SYNTAX'Unds'OpCode{}(),Lbl'UndsSClnUndsUnds'LIST-CONS-SYNTAX'Unds'OpCodes'Unds'OpCode'Unds'OpCodes{}(Lblstore'Unds'LIST-CONS-SYNTAX'Unds'OpCode{}(),Lbl'Stop'OpCodes'Unds'LIST-CONS-SYNTAX'Unds'OpCodes{}()))]
diff --git a/test/output/list-factory/input.proof.out.diff b/test/output/list-factory/input.proof.out.diff
index acabc21aa..0de1beff8 100644
--- a/test/output/list-factory/input.proof.out.diff
+++ b/test/output/list-factory/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'Hash'revOps'LParUndsRParUnds'LIST-FACTORY-SYNTAX'Unds'OpCodes'Unds'OpCodes{} ()
 rule: 2692 1
   VarOPS = kore[Lbl'UndsSClnUndsUnds'LIST-FACTORY-SYNTAX'Unds'OpCodes'Unds'OpCode'Unds'OpCodes{}(Lblload'Unds'LIST-FACTORY-SYNTAX'Unds'OpCode{}(),Lbl'UndsSClnUndsUnds'LIST-FACTORY-SYNTAX'Unds'OpCodes'Unds'OpCode'Unds'OpCodes{}(Lblstore'Unds'LIST-FACTORY-SYNTAX'Unds'OpCode{}(),Lbl'UndsSClnUndsUnds'LIST-FACTORY-SYNTAX'Unds'OpCodes'Unds'OpCode'Unds'OpCodes{}(LblnoOp'Unds'LIST-FACTORY-SYNTAX'Unds'OpCode{}(),Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'LIST-FACTORY-SYNTAX'Unds'OpCodes'Unds'OpCode'Unds'OpCodes'QuotRBraUnds'OpCodes{}())))]
diff --git a/test/output/list-semantic/input.proof.out.diff b/test/output/list-semantic/input.proof.out.diff
index f5790c5ed..0aadcd363 100644
--- a/test/output/list-semantic/input.proof.out.diff
+++ b/test/output/list-semantic/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: LIST.element LblListItem{} ()
   function: LblListItem{} ()
   arg: kore[LblnoOp'Unds'LIST-SEMANTIC-SYNTAX'Unds'OpCode{}()]
diff --git a/test/output/macro/inrange.proof.out.diff b/test/output/macro/inrange.proof.out.diff
index dd4339ed2..31de76fd4 100644
--- a/test/output/macro/inrange.proof.out.diff
+++ b/test/output/macro/inrange.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: LblinRange'LParUndsRParUnds'MACRO-SYNTAX'Unds'Bool'Unds'Int{} ()
 rule: 151 1
   VarX = kore[\dv{SortInt{}}("10")]
diff --git a/test/output/map-fun/ac-hard.proof.out.diff b/test/output/map-fun/ac-hard.proof.out.diff
index 00f036097..73256ba7b 100644
--- a/test/output/map-fun/ac-hard.proof.out.diff
+++ b/test/output/map-fun/ac-hard.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortInt{}}("5")]
diff --git a/test/output/map-fun/ac.proof.out.diff b/test/output/map-fun/ac.proof.out.diff
index bb79f878e..14fcc5d64 100644
--- a/test/output/map-fun/ac.proof.out.diff
+++ b/test/output/map-fun/ac.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortInt{}}("3")]
diff --git a/test/output/map-fun/acu-hard.proof.out.diff b/test/output/map-fun/acu-hard.proof.out.diff
index 70d5fc0ec..32381ecee 100644
--- a/test/output/map-fun/acu-hard.proof.out.diff
+++ b/test/output/map-fun/acu-hard.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.unit Lbl'Stop'Map{} ()
   function: Lbl'Stop'Map{} ()
 hook result: kore[Lbl'Stop'Map{}()]
diff --git a/test/output/map-fun/comm.proof.out.diff b/test/output/map-fun/comm.proof.out.diff
index f4094344d..3ed539a64 100644
--- a/test/output/map-fun/comm.proof.out.diff
+++ b/test/output/map-fun/comm.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortInt{}}("2")]
diff --git a/test/output/map-fun/no-acu.proof.out.diff b/test/output/map-fun/no-acu.proof.out.diff
index 27c0b11d0..47cf6b963 100644
--- a/test/output/map-fun/no-acu.proof.out.diff
+++ b/test/output/map-fun/no-acu.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortInt{}}("2")]
diff --git a/test/output/map-fun/unit.proof.out.diff b/test/output/map-fun/unit.proof.out.diff
index 5c116f935..df180d9c5 100644
--- a/test/output/map-fun/unit.proof.out.diff
+++ b/test/output/map-fun/unit.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortInt{}}("1")]
diff --git a/test/output/memo-function/input.proof.out.diff b/test/output/memo-function/input.proof.out.diff
index 8f51077e2..48ca5d130 100644
--- a/test/output/memo-function/input.proof.out.diff
+++ b/test/output/memo-function/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblnext'LParUndsRParUnds'MEMO-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo{} ()
 rule: 127 0
 function: Lblnext'LParUndsRParUnds'MEMO-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo{} ()
diff --git a/test/output/modular-config/exec.proof.out.diff b/test/output/modular-config/exec.proof.out.diff
index 6609ab707..c16c8035a 100644
--- a/test/output/modular-config/exec.proof.out.diff
+++ b/test/output/modular-config/exec.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/nested-cells/exec.proof.out.diff b/test/output/nested-cells/exec.proof.out.diff
index 02b07599f..9586d2faf 100644
--- a/test/output/nested-cells/exec.proof.out.diff
+++ b/test/output/nested-cells/exec.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/non-rec-function/input.proof.out.diff b/test/output/non-rec-function/input.proof.out.diff
index 57195e876..5b3a58a6e 100644
--- a/test/output/non-rec-function/input.proof.out.diff
+++ b/test/output/non-rec-function/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/pcf/collatz.proof.out.diff b/test/output/pcf/collatz.proof.out.diff
index 65e92d5df..36f99c4dd 100644
--- a/test/output/pcf/collatz.proof.out.diff
+++ b/test/output/pcf/collatz.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/pcf/exp.proof.out.diff b/test/output/pcf/exp.proof.out.diff
index 812e7f011..1e3214c3b 100644
--- a/test/output/pcf/exp.proof.out.diff
+++ b/test/output/pcf/exp.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl-'UndsUnds'PCF-SYNTAX'Unds'Int'Unds'Int{} ()
 rule: 2843 1
   VarV = kore[\dv{SortInt{}}("1")]
diff --git a/test/output/peano/mul_3_5.proof.out.diff b/test/output/peano/mul_3_5.proof.out.diff
index 428709b1e..8f3982cb8 100644
--- a/test/output/peano/mul_3_5.proof.out.diff
+++ b/test/output/peano/mul_3_5.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/prioritized-rule/foo-a.proof.out.diff b/test/output/prioritized-rule/foo-a.proof.out.diff
index df732144e..f4333c36e 100644
--- a/test/output/prioritized-rule/foo-a.proof.out.diff
+++ b/test/output/prioritized-rule/foo-a.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/projection/input.proof.out.diff b/test/output/projection/input.proof.out.diff
index ccbb8195f..94e5ca3ad 100644
--- a/test/output/projection/input.proof.out.diff
+++ b/test/output/projection/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/reg/exec.proof.out.diff b/test/output/reg/exec.proof.out.diff
index 93ed881c1..2dcbfff6a 100644
--- a/test/output/reg/exec.proof.out.diff
+++ b/test/output/reg/exec.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/set-fun/input.proof.out.diff b/test/output/set-fun/input.proof.out.diff
index eefd51384..af0dfb7f8 100644
--- a/test/output/set-fun/input.proof.out.diff
+++ b/test/output/set-fun/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: SET.element LblSetItem{} ()
   function: LblSetItem{} ()
   arg: kore[Lblc'Unds'SET-FUN-SYNTAX'Unds'Key{}()]
diff --git a/test/output/simple/input.proof.out.diff b/test/output/simple/input.proof.out.diff
index cd5ee7940..f1a5fd033 100644
--- a/test/output/simple/input.proof.out.diff
+++ b/test/output/simple/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lblf'LParUndsRParUnds'SIMPLE'Unds'Expr'Unds'Int{} ()
 rule: 2725 1
   Var'Unds'Gen0 = kore[\dv{SortInt{}}("0")]
diff --git a/test/output/single-rewrite/foo-a.proof.out.diff b/test/output/single-rewrite/foo-a.proof.out.diff
index b90497a5b..7d179a152 100644
--- a/test/output/single-rewrite/foo-a.proof.out.diff
+++ b/test/output/single-rewrite/foo-a.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/sum-cell/in.proof.out.diff b/test/output/sum-cell/in.proof.out.diff
index 6890c98c9..659d3dee6 100644
--- a/test/output/sum-cell/in.proof.out.diff
+++ b/test/output/sum-cell/in.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/tree-reverse-int/reverse-one-five.proof.out.diff b/test/output/tree-reverse-int/reverse-one-five.proof.out.diff
index 4c7b511f3..045a4c57f 100644
--- a/test/output/tree-reverse-int/reverse-one-five.proof.out.diff
+++ b/test/output/tree-reverse-int/reverse-one-five.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/tree-reverse-int/reverse-one.proof.out.diff b/test/output/tree-reverse-int/reverse-one.proof.out.diff
index ca7484127..f3e11782c 100644
--- a/test/output/tree-reverse-int/reverse-one.proof.out.diff
+++ b/test/output/tree-reverse-int/reverse-one.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/tree-reverse/simplify.proof.out.diff b/test/output/tree-reverse/simplify.proof.out.diff
index 618c76524..7aad745ac 100644
--- a/test/output/tree-reverse/simplify.proof.out.diff
+++ b/test/output/tree-reverse/simplify.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/two-counters/10.proof.out.diff b/test/output/two-counters/10.proof.out.diff
index e1863f998..071db705a 100644
--- a/test/output/two-counters/10.proof.out.diff
+++ b/test/output/two-counters/10.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
diff --git a/test/output/type-cast/input.proof.out.diff b/test/output/type-cast/input.proof.out.diff
index ad744605b..09f57408f 100644
--- a/test/output/type-cast/input.proof.out.diff
+++ b/test/output/type-cast/input.proof.out.diff
@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]