Merge remote-tracking branch 'origin/develop'

bindings/python/ast.cpp

@@ -373,9 +373,12 @@ void bind_parser(py::module_ &mod) {
           "pattern",
           [](kore_parser &parser) { return std::shared_ptr(parser.pattern()); })
       .def("sort", [](kore_parser &parser) { return parser.sort(); })
-      .def("definition", [](kore_parser &parser) {
-        return std::shared_ptr(parser.definition());
-      });
+      .def(
+          "definition",
+          [](kore_parser &parser) {
+            return std::shared_ptr(parser.definition());
+          })
+      .def("symbol", &kore_parser::symbol);
 }
 
 void bind_proof_trace(py::module_ &m) {
@@ -421,6 +424,7 @@ void bind_proof_trace(py::module_ &m) {
   py::class_<llvm_hook_event, std::shared_ptr<llvm_hook_event>>(
       proof_trace, "llvm_hook_event", step_event)
       .def_property_readonly("name", &llvm_hook_event::get_name)
+      .def_property_readonly("symbol_name", &llvm_hook_event::get_symbol_name)
       .def_property_readonly(
           "relative_position", &llvm_hook_event::get_relative_position)
       .def_property_readonly("args", &llvm_hook_event::get_arguments)

docs/proof-trace.md

@@ -48,7 +48,8 @@ name              ::= string
 location          ::= string
 function          ::= WORD(0xDD) name location arg* WORD(0x11) // the arg list is ommited in normal mode
 
-hook              ::= WORD(0xAA) name location arg* WORD(0xBB) kore_term
+symbol_name       ::= string
+hook              ::= WORD(0xAA) name symbol_name location arg* WORD(0xBB) kore_term
 
 ordinal           ::= uint64
 arity             ::= uint64

include/kllvm/binary/ProofTraceParser.h

@@ -159,20 +159,27 @@ class llvm_function_event : public llvm_step_event {
 class llvm_hook_event : public llvm_step_event {
 private:
   std::string name_;
+  std::string symbol_name_;
   std::string relative_position_;
   std::vector<llvm_event> arguments_;
   sptr<kore_pattern> kore_pattern_;
   uint64_t pattern_length_{0U};
 
-  llvm_hook_event(std::string name, std::string relative_position);
+  llvm_hook_event(
+      std::string name, std::string symbol_name, std::string relative_position);
 
 public:
-  static sptr<llvm_hook_event>
-  create(std::string const &name, std::string const &relative_position) {
-    return sptr<llvm_hook_event>(new llvm_hook_event(name, relative_position));
+  static sptr<llvm_hook_event> create(
+      std::string const &name, std::string const &symbol_name,
+      std::string const &relative_position) {
+    return sptr<llvm_hook_event>(
+        new llvm_hook_event(name, symbol_name, relative_position));
   }
 
   [[nodiscard]] std::string const &get_name() const { return name_; }
+  [[nodiscard]] std::string const &get_symbol_name() const {
+    return symbol_name_;
+  }
   [[nodiscard]] std::string const &get_relative_position() const {
     return relative_position_;
   }
@@ -260,7 +267,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 9U;
+  static constexpr uint32_t expected_version = 10U;
 
 private:
   bool verbose_;
@@ -415,12 +422,17 @@ class proof_trace_parser {
       return nullptr;
     }
 
+    std::string symbol_name;
+    if (!parse_name(ptr, end, symbol_name)) {
+      return nullptr;
+    }
+
     std::string location;
     if (!parse_location(ptr, end, location)) {
       return nullptr;
     }
 
-    auto event = llvm_hook_event::create(name, location);
+    auto event = llvm_hook_event::create(name, symbol_name, location);
 
     while (std::distance(ptr, end) < 8U
            || peek_word(ptr) != hook_result_sentinel) {

include/kllvm/codegen/ProofEvent.h

@@ -92,8 +92,8 @@ class proof_event {
 
 public:
   [[nodiscard]] llvm::BasicBlock *hook_event_pre(
-      std::string const &name, llvm::BasicBlock *current_block,
-      std::string const &location_stack);
+      std::string const &name, kore_composite_pattern *pattern,
+      llvm::BasicBlock *current_block, std::string const &location_stack);
 
   [[nodiscard]] llvm::BasicBlock *hook_event_post(
       llvm::Value *val, kore_composite_sort *sort,

include/kllvm/parser/KOREParser.h

@@ -23,6 +23,7 @@ class kore_parser {
   ptr<kore_definition> definition();
   sptr<kore_pattern> pattern();
   sptr<kore_sort> sort();
+  ptr<kore_symbol> symbol();
   std::vector<ptr<kore_declaration>> declarations();
 
   std::pair<std::string, std::vector<sptr<kore_sort>>> symbol_sort_list();

lib/binary/ProofTraceParser.cpp

@@ -20,8 +20,9 @@ void llvm_function_event::add_argument(llvm_event const &argument) {
 }
 
 llvm_hook_event::llvm_hook_event(
-    std::string name, std::string relative_position)
+    std::string name, std::string symbol_name, std::string relative_position)
     : name_(std::move(name))
+    , symbol_name_(std::move(symbol_name))
     , relative_position_(std::move(relative_position))
     , kore_pattern_(nullptr) { }
 
@@ -81,7 +82,8 @@ void llvm_function_event::print(
 void llvm_hook_event::print(
     std::ostream &out, bool expand_terms, unsigned ind) const {
   std::string indent(ind * indent_size, ' ');
-  out << fmt::format("{}hook: {} ({})\n", indent, name_, relative_position_);
+  out << fmt::format(
+      "{}hook: {} {} ({})\n", indent, name_, symbol_name_, relative_position_);
   for (auto const &arg : arguments_) {
     arg.print(out, expand_terms, true, ind + 1U);
   }

lib/codegen/CreateTerm.cpp

@@ -938,7 +938,8 @@ std::pair<llvm::Value *, bool> create_term::create_allocation(
         std::string name = str_pattern->get_contents();
 
         proof_event p(definition_, module_);
-        current_block_ = p.hook_event_pre(name, current_block_, location_stack);
+        current_block_ = p.hook_event_pre(
+            name, constructor, current_block_, location_stack);
         llvm::Value *val = create_hook(
             symbol_decl->attributes().get(attribute_set::key::Hook).get(),
             constructor, location_stack);

lib/codegen/ProofEvent.cpp

@@ -166,8 +166,8 @@ proof_event::event_prelude(
  */
 
 llvm::BasicBlock *proof_event::hook_event_pre(
-    std::string const &name, llvm::BasicBlock *current_block,
-    std::string const &location_stack) {
+    std::string const &name, kore_composite_pattern *pattern,
+    llvm::BasicBlock *current_block, std::string const &location_stack) {
   if (!proof_hint_instrumentation) {
     return current_block;
   }
@@ -177,6 +177,8 @@ llvm::BasicBlock *proof_event::hook_event_pre(
 
   emit_write_uint64(outputFile, detail::word(0xAA), true_block);
   emit_write_string(outputFile, name, true_block);
+  emit_write_string(
+      outputFile, ast_to_string(*pattern->get_constructor()), true_block);
   emit_write_string(outputFile, location_stack, true_block);
 
   llvm::BranchInst::Create(merge_block, true_block);

lib/parser/KOREParser.cpp

@@ -343,12 +343,7 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
     consume(token::LeftBrace);
     consume(token::RightBrace);
     consume(token::LeftParen);
-    std::string symbol = consume(token::Id);
-    consume(token::LeftBrace);
-    auto pat = kore_composite_pattern::create(symbol);
-    sorts(pat->get_constructor());
-    pat->get_constructor()->init_pattern_arguments();
-    consume(token::RightBrace);
+    auto sym = symbol();
     consume(token::LeftParen);
     std::vector<sptr<kore_pattern>> pats;
     patterns(pats);
@@ -358,7 +353,7 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
       sptr<kore_pattern> accum = pats[0];
       for (auto i = 1U; i < pats.size(); i++) {
         sptr<kore_composite_pattern> new_accum
-            = kore_composite_pattern::create(pat->get_constructor());
+            = kore_composite_pattern::create(sym.get());
         new_accum->add_argument(accum);
         new_accum->add_argument(pats[i]);
         accum = new_accum;
@@ -368,7 +363,7 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
     sptr<kore_pattern> accum = pats[pats.size() - 1];
     for (int i = pats.size() - 2; i >= 0; i--) {
       sptr<kore_composite_pattern> new_accum
-          = kore_composite_pattern::create(pat->get_constructor());
+          = kore_composite_pattern::create(sym.get());
       new_accum->add_argument(pats[i]);
       new_accum->add_argument(accum);
       accum = new_accum;
@@ -402,6 +397,16 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
   return result;
 }
 
+ptr<kore_symbol> kore_parser::symbol() {
+  std::string symbol = consume(token::Id);
+  consume(token::LeftBrace);
+  auto pat = kore_composite_pattern::create(symbol);
+  sorts(pat->get_constructor());
+  pat->get_constructor()->init_pattern_arguments();
+  consume(token::RightBrace);
+  return std::make_unique<kore_symbol>(*pat->get_constructor());
+}
+
 ptr<kore_composite_pattern>
 kore_parser::application_pattern_internal(std::string const &name) {
   consume(token::LeftBrace);

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 = 9;
+  uint32_t version = 10;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }

test/lit.cfg.py

@@ -168,6 +168,7 @@ def one_line(s):
             in=%test-dir-in/`basename $out .proof.out.diff`.in
             rm -f %t.out.bin
             hint=%t.`basename $out .proof.out.diff`.hint
+            rm -f $hint
             %t.interpreter $in -1 $hint --proof-output
             %kore-proof-trace --verbose --expand-terms %t.header.bin $hint | diff - $out
             result="$?"

test/output/add-rewrite/input.proof.out.diff

@@ -1,13 +1,13 @@
-version: 9
-hook: MAP.element ()
+version: 10
+hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
   arg: kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
 hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
-hook: MAP.unit ()
+hook: MAP.unit Lbl'Stop'Map{} ()
   function: Lbl'Stop'Map{} ()
 hook result: kore[Lbl'Stop'Map{}()]
-hook: MAP.concat ()
+hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   function: Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
@@ -19,7 +19,7 @@ function: LblinitKCell{} (0)
 rule: 112 1
   VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
 function: Lblproject'Coln'KItem{} (0:0)
-  hook: MAP.lookup (0:0:0:0)
+  hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
     function: LblMap'Coln'lookup{} (0:0:0:0)
     arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
     arg: kore[\dv{SortKConfigVar{}}("$PGM")]

test/output/arith/add.proof.out.diff

@@ -1,13 +1,13 @@
-version: 9
-hook: MAP.element ()
+version: 10
+hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]
   arg: kore[Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2")))]
 hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))))]
-hook: MAP.unit ()
+hook: MAP.unit Lbl'Stop'Map{} ()
   function: Lbl'Stop'Map{} ()
 hook result: kore[Lbl'Stop'Map{}()]
-hook: MAP.concat ()
+hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   function: Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))))]
@@ -19,7 +19,7 @@ function: LblinitKCell{} (0)
 rule: 2804 1
   VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))))]
 function: Lblproject'Coln'KItem{} (0:0)
-  hook: MAP.lookup (0:0:0:0)
+  hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
     function: LblMap'Coln'lookup{} (0:0:0:0)
     arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))))]
     arg: kore[\dv{SortKConfigVar{}}("$PGM")]
@@ -31,9 +31,9 @@ rule: 2802 0
 config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
 side condition entry: 2746 1
   VarHOLE = kore[\dv{SortInt{}}("1")]
-hook: BOOL.and ()
+hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
   arg: kore[\dv{SortBool{}}("true")]
-  hook: BOOL.not (1)
+  hook: BOOL.not LblnotBool'Unds'{} (1)
     function: LblisKResult{} (1:0)
     rule: 2841 1
       VarKResult = kore[\dv{SortInt{}}("1")]
@@ -44,9 +44,9 @@ hook result: kore[\dv{SortBool{}}("false")]
 side condition exit: 2746 false
 side condition entry: 2747 1
   VarHOLE = kore[Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))]
-hook: BOOL.and ()
+hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
   arg: kore[\dv{SortBool{}}("true")]
-  hook: BOOL.not (1)
+  hook: BOOL.not LblnotBool'Unds'{} (1)
     function: LblisKResult{} (1:0)
     rule: 2840 1
       VarK = kore[kseq{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2")),dotk{}())]
@@ -62,9 +62,9 @@ rule: 2747 4
   VarK0 = kore[\dv{SortInt{}}("1")]
 side condition entry: 2746 1
   VarHOLE = kore[\dv{SortInt{}}("1")]
-hook: BOOL.and ()
+hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
   arg: kore[\dv{SortBool{}}("true")]
-  hook: BOOL.not (1)
+  hook: BOOL.not LblnotBool'Unds'{} (1)
     function: LblisKResult{} (1:0)
     rule: 2841 1
       VarKResult = kore[\dv{SortInt{}}("1")]
@@ -75,9 +75,9 @@ hook result: kore[\dv{SortBool{}}("false")]
 side condition exit: 2746 false
 side condition entry: 2747 1
   VarHOLE = kore[\dv{SortInt{}}("2")]
-hook: BOOL.and ()
+hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
   arg: kore[\dv{SortBool{}}("true")]
-  hook: BOOL.not (1)
+  hook: BOOL.not LblnotBool'Unds'{} (1)
     function: LblisKResult{} (1:0)
     rule: 2841 1
       VarKResult = kore[\dv{SortInt{}}("2")]
@@ -91,14 +91,14 @@ rule: 2748 4
   Var'Unds'DotVar1 = kore[kseq{}(Lbl'Hash'freezeradd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp1'Unds'{}(kseq{}(\dv{SortInt{}}("1"),dotk{}())),dotk{}())]
   VarA = kore[\dv{SortInt{}}("1")]
   VarB = kore[\dv{SortInt{}}("2")]
-hook: INT.add (0:0:0)
+hook: INT.add Lbl'UndsPlus'Int'Unds'{} (0:0:0)
   function: Lbl'UndsPlus'Int'Unds'{} (0:0:0)
   arg: kore[\dv{SortInt{}}("1")]
   arg: kore[\dv{SortInt{}}("2")]
 hook result: kore[\dv{SortInt{}}("3")]
 side condition entry: 2740 1
   Var'Unds'Gen2 = kore[\dv{SortInt{}}("3")]
-hook: BOOL.and ()
+hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
   arg: kore[\dv{SortBool{}}("true")]
   function: LblisKResult{} (1)
   rule: 2841 1
@@ -114,9 +114,9 @@ rule: 2740 5
   VarK0 = kore[\dv{SortInt{}}("1")]
 side condition entry: 2746 1
   VarHOLE = kore[\dv{SortInt{}}("1")]
-hook: BOOL.and ()
+hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
   arg: kore[\dv{SortBool{}}("true")]
-  hook: BOOL.not (1)
+  hook: BOOL.not LblnotBool'Unds'{} (1)
     function: LblisKResult{} (1:0)
     rule: 2841 1
       VarKResult = kore[\dv{SortInt{}}("1")]
@@ -127,9 +127,9 @@ hook result: kore[\dv{SortBool{}}("false")]
 side condition exit: 2746 false
 side condition entry: 2747 1
   VarHOLE = kore[\dv{SortInt{}}("3")]
-hook: BOOL.and ()
+hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
   arg: kore[\dv{SortBool{}}("true")]
-  hook: BOOL.not (1)
+  hook: BOOL.not LblnotBool'Unds'{} (1)
     function: LblisKResult{} (1:0)
     rule: 2841 1
       VarKResult = kore[\dv{SortInt{}}("3")]
@@ -143,7 +143,7 @@ rule: 2748 4
   Var'Unds'DotVar1 = kore[dotk{}()]
   VarA = kore[\dv{SortInt{}}("1")]
   VarB = kore[\dv{SortInt{}}("3")]
-hook: INT.add (0:0:0)
+hook: INT.add Lbl'UndsPlus'Int'Unds'{} (0:0:0)
   function: Lbl'UndsPlus'Int'Unds'{} (0:0:0)
   arg: kore[\dv{SortInt{}}("1")]
   arg: kore[\dv{SortInt{}}("3")]