runtimeverification · rv-jenkins · May 31, 2024 · May 31, 2024
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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'{} ()