Merge remote-tracking branch 'origin/develop'

runtimeverification · Sep 23, 2024 · c262351 · c262351
2 parents c023bc5 + c23fb6f
commit c262351
Show file tree

Hide file tree

Showing 104 changed files with 11 additions and 4,291 deletions.
diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp
@@ -693,6 +693,12 @@ llvm::Value *create_term::create_hardcoded_hook(
   return nullptr;
 }
 
+static bool hook_is_collection_unit_or_element(std::string const &name) {
+  return name == "LIST.unit" || name == "LIST.element" || name == "MAP.unit"
+         || name == "MAP.element" || name == "SET.unit" || name == "SET.element"
+         || name == "RANGEMAP.unit" || name == "RANGEMAP.element";
+}
+
 llvm::Value *create_term::create_hook(
     kore_composite_pattern *hook_att, kore_composite_pattern *pattern,
     std::string const &location_stack) {
@@ -715,6 +721,11 @@ llvm::Value *create_term::create_hook(
     enable_gc(old_val);
   }
 
+  if (hook_is_collection_unit_or_element(name)) {
+    // no proof trace event generation for unit/element collection hooks
+    return result;
+  }
+
   proof_event e(definition_, module_);
   current_block_
       = e.hook_event_pre(name, pattern, current_block_, location_stack);

diff --git a/test/output/add-rewrite/input.proof.debug.out.diff b/test/output/add-rewrite/input.proof.debug.out.diff
@@ -1,10 +1,4 @@
 version: 13
-hook: MAP.element 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 Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat 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{}()))]

diff --git a/test/output/add-rewrite/input.proof.out.diff b/test/output/add-rewrite/input.proof.out.diff
@@ -1,10 +1,4 @@
 version: 13
-hook: MAP.element 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 Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat 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{}()))]

diff --git a/test/output/arith/add.proof.out.diff b/test/output/arith/add.proof.out.diff
@@ -1,10 +1,4 @@
 version: 13
-hook: MAP.element 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 Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat 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"))))]

diff --git a/test/output/arith/well.proof.out.diff b/test/output/arith/well.proof.out.diff
@@ -1,10 +1,4 @@
 version: 13
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lblwell'LParUndsCommUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp'Unds'Exp{}(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"))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("5"),\dv{SortInt{}}("10")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("3"),\dv{SortInt{}}("4")))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblwell'LParUndsCommUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp'Unds'Exp{}(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"))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("5"),\dv{SortInt{}}("10")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("3"),\dv{SortInt{}}("4"))))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblwell'LParUndsCommUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp'Unds'Exp{}(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"))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("5"),\dv{SortInt{}}("10")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("3"),\dv{SortInt{}}("4"))))]

diff --git a/test/output/assoc-function/left.proof.out.diff b/test/output/assoc-function/left.proof.out.diff
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Und
 rule: 103 2
   Var'Unds'X = kore[Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
   VarY = kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbld'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
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Und
 rule: 103 2
   Var'Unds'X = kore[Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
   VarY = kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbld'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
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Un
 rule: 104 2
   Var'Unds'Y = kore[Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
   VarX = kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbla'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
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Un
 rule: 104 2
   Var'Unds'Y = kore[Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
   VarX = kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbla'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
@@ -14,12 +14,6 @@ hook: KEQUAL.ite Lblite{SortInt{}} ()
   arg: kore[\dv{SortBool{}}("true")]
   arg: kore[\dv{SortInt{}}("5")]
 hook result: kore[\dv{SortInt{}}("5")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[\dv{SortInt{}}("5")]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortInt{}}("5"))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortInt{}}("5"))]

diff --git a/test/output/builtin-functions/double.proof.out.diff b/test/output/builtin-functions/double.proof.out.diff
@@ -6,12 +6,6 @@ hook: INT.mul Lbl'UndsStar'Int'Unds'{} ()
   arg: kore[\dv{SortInt{}}("5")]
   arg: kore[\dv{SortInt{}}("2")]
 hook result: kore[\dv{SortInt{}}("10")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[\dv{SortInt{}}("10")]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortInt{}}("10"))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortInt{}}("10"))]

diff --git a/test/output/builtin-functions/head-bytes.proof.out.diff b/test/output/builtin-functions/head-bytes.proof.out.diff
@@ -7,12 +7,6 @@ hook: BYTES.substr LblsubstrBytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'
   arg: kore[\dv{SortInt{}}("0")]
   arg: kore[\dv{SortInt{}}("1")]
 hook result: kore[\dv{SortBytes{}}("b")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[\dv{SortBytes{}}("b")]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortBytes{}}("b"))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortBytes{}}("b"))]

diff --git a/test/output/builtin-functions/head-string.proof.out.diff b/test/output/builtin-functions/head-string.proof.out.diff
@@ -7,12 +7,6 @@ hook: STRING.substr LblsubstrString'LParUndsCommUndsCommUndsRParUnds'STRING-COMM
   arg: kore[\dv{SortInt{}}("0")]
   arg: kore[\dv{SortInt{}}("1")]
 hook result: kore[\dv{SortString{}}("s")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[\dv{SortString{}}("s")]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("s"))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("s"))]

diff --git a/test/output/builtin-functions/ispos.proof.out.diff b/test/output/builtin-functions/ispos.proof.out.diff
@@ -6,12 +6,6 @@ hook: INT.gt Lbl'Unds-GT-'Int'Unds'{} ()
   arg: kore[\dv{SortInt{}}("0")]
   arg: kore[\dv{SortInt{}}("0")]
 hook result: kore[\dv{SortBool{}}("false")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[\dv{SortBool{}}("false")]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortBool{}}("false"))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortBool{}}("false"))]

diff --git a/test/output/builtin-functions/next-abs.proof.out.diff b/test/output/builtin-functions/next-abs.proof.out.diff
@@ -14,12 +14,6 @@ hook: KEQUAL.ite Lblite{SortInt{}} ()
   arg: kore[\dv{SortBool{}}("true")]
   arg: kore[\dv{SortInt{}}("5")]
 hook result: kore[\dv{SortInt{}}("5")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortInt{}}("5"))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortInt{}}("5")))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\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
@@ -6,12 +6,6 @@ hook: INT.mul Lbl'UndsStar'Int'Unds'{} ()
   arg: kore[\dv{SortInt{}}("5")]
   arg: kore[\dv{SortInt{}}("2")]
 hook result: kore[\dv{SortInt{}}("10")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortInt{}}("10"))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortInt{}}("10")))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortInt{}}("10")))]

diff --git a/test/output/builtin-functions/next-head-bytes.proof.out.diff b/test/output/builtin-functions/next-head-bytes.proof.out.diff
@@ -7,12 +7,6 @@ hook: BYTES.substr LblsubstrBytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'
   arg: kore[\dv{SortInt{}}("0")]
   arg: kore[\dv{SortInt{}}("1")]
 hook result: kore[\dv{SortBytes{}}("b")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortBytes{}}("b"))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortBytes{}}("b")))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortBytes{}}("b")))]

diff --git a/test/output/builtin-functions/next-head-string.proof.out.diff b/test/output/builtin-functions/next-head-string.proof.out.diff
@@ -7,12 +7,6 @@ hook: STRING.substr LblsubstrString'LParUndsCommUndsCommUndsRParUnds'STRING-COMM
   arg: kore[\dv{SortInt{}}("0")]
   arg: kore[\dv{SortInt{}}("1")]
 hook result: kore[\dv{SortString{}}("s")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortString{}}("s"))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortString{}}("s")))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortString{}}("s")))]

diff --git a/test/output/builtin-functions/next-ispos.proof.out.diff b/test/output/builtin-functions/next-ispos.proof.out.diff
@@ -6,12 +6,6 @@ hook: INT.gt Lbl'Unds-GT-'Int'Unds'{} ()
   arg: kore[\dv{SortInt{}}("0")]
   arg: kore[\dv{SortInt{}}("0")]
 hook result: kore[\dv{SortBool{}}("false")]
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortBool{}}("false"))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortBool{}}("false")))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'KItem'Unds'KItem{}(\dv{SortBool{}}("false")))]

diff --git a/test/output/builtin-hook-events/program.proof.out.diff b/test/output/builtin-hook-events/program.proof.out.diff
@@ -1,10 +1,4 @@
 version: 13
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lblfoo'LParUndsRParUnds'BUILTIN-HOOK-EVENTS-SYNTAX'Unds'Foo'Unds'Bool{}(\dv{SortBool{}}("true"))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblfoo'LParUndsRParUnds'BUILTIN-HOOK-EVENTS-SYNTAX'Unds'Foo'Unds'Bool{}(\dv{SortBool{}}("true")))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblfoo'LParUndsRParUnds'BUILTIN-HOOK-EVENTS-SYNTAX'Unds'Foo'Unds'Bool{}(\dv{SortBool{}}("true")))]

diff --git a/test/output/builtin-int/input.proof.out.diff b/test/output/builtin-int/input.proof.out.diff
@@ -1,10 +1,4 @@
 version: 13
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[Lblsucc'LParUndsRParUnds'BUILTIN-INT-SYNTAX'Unds'Foo'Unds'Foo{}(Lblfoo'LParUndsRParUnds'BUILTIN-INT-SYNTAX'Unds'Foo'Unds'Int{}(\dv{SortInt{}}("5")))]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblsucc'LParUndsRParUnds'BUILTIN-INT-SYNTAX'Unds'Foo'Unds'Foo{}(Lblfoo'LParUndsRParUnds'BUILTIN-INT-SYNTAX'Unds'Foo'Unds'Int{}(\dv{SortInt{}}("5"))))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblsucc'LParUndsRParUnds'BUILTIN-INT-SYNTAX'Unds'Foo'Unds'Foo{}(Lblfoo'LParUndsRParUnds'BUILTIN-INT-SYNTAX'Unds'Foo'Unds'Int{}(\dv{SortInt{}}("5"))))]

diff --git a/test/output/builtin-io/read.proof.intermediate.out.diff b/test/output/builtin-io/read.proof.intermediate.out.diff
@@ -1,10 +1,4 @@
 version: 13
-hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
-  arg: kore[\dv{SortString{}}("input_file")]
-hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
-hook: MAP.unit Lbl'Stop'Map{} ()
-hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]