From c2ca9eb05722fcfcaa0bf1b32fdb4ee313f7224c Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@runtimeverification.com>
Date: Wed, 23 Oct 2024 20:14:19 +0300
Subject: [PATCH] tmp

---
 Dockerfile                      | 3 +--
 ukm-semantics/test/execution.md | 8 --------
 2 files changed, 1 insertion(+), 10 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 5c59231..305329a 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -8,8 +8,7 @@ FROM runtimeverificationinc/kframework-k:ubuntu-noble-${K_COMMIT}
 RUN    apt-get update              \
     && apt-get upgrade --yes       \
     && apt-get install --yes       \
-                       curl \
-                       libcrypto++-dev
+                       curl
 
 ARG USER_ID=1001
 ARG GROUP_ID=1001
diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md
index b1611f9..77956e4 100644
--- a/ukm-semantics/test/execution.md
+++ b/ukm-semantics/test/execution.md
@@ -5,8 +5,6 @@ module UKM-TEST-SYNTAX
     imports RUST-EXECUTION-TEST-PARSING-SYNTAX
     imports UKM-HOOKS-UKM-SYNTAX
 
-    syntax UkmInstruction ::= "ukmDecodePreprocessedCell"
-
     syntax ExecutionItem  ::= "mock" "CallData"
                             | "mock" "Caller"
                             | "mock" UkmHook UkmHookResult
@@ -29,8 +27,6 @@ endmodule
 module UKM-TEST-EXECUTION
     imports private COMMON-K-CELL
     imports private RUST-EXECUTION-TEST-CONFIGURATION
-    imports private UKM-DECODING-SYNTAX
-    imports private UKM-ENCODING-SYNTAX
     imports private UKM-EXECUTION-SYNTAX
     imports private UKM-HOOKS-BYTES-CONFIGURATION
     imports private UKM-HOOKS-BYTES-SYNTAX
@@ -39,10 +35,6 @@ module UKM-TEST-EXECUTION
     imports private UKM-HOOKS-UKM-SYNTAX
     imports private UKM-TEST-SYNTAX
 
-    // Patching the encoding result to decoding for test purposes
-    rule ukmEncodedPreprocessedCell(B:Bytes) ~> ukmDecodePreprocessedCell
-        => ukmDecodePreprocessedCell(B)
-
     syntax Mockable ::= UkmHook
 
     rule