diff --git a/kmxwasm/k-src/ceils-syntax.k b/kmxwasm/k-src/ceils-syntax.k
index d967b1ee..b4684d4b 100644
--- a/kmxwasm/k-src/ceils-syntax.k
+++ b/kmxwasm/k-src/ceils-syntax.k
@@ -8,10 +8,12 @@ module CEILS-SYNTAX
     syntax Bool ::= definedReplaceAtBytes(dest: Bytes, index: Int, src: Bytes)  [function, total]
     syntax Bool ::= definedPadRightBytes(Bytes, length: Int, value: Int)  [function, total]
     syntax Bool ::= definedModInt(Int, Int)  [function, total]
+    syntax Bool ::= definedDivInt(Int, Int)  [function, total]
     syntax Bool ::= definedShlInt(Int, Int)  [function, total]
     syntax Bool ::= definedShrInt(Int, Int)  [function, total]
     syntax Bool ::= definedPowInt(Int, Int)  [function, total]
-    syntax Bool ::= definedDivInt(Int, Int)  [function, total]
+    syntax Bool ::= definedTModInt(Int, Int)  [function, total]
+    syntax Bool ::= definedTDivInt(Int, Int)  [function, total]
     syntax Bool ::= definedLog2Int(Int)  [function, total]
     syntax Bool ::= definedProjectBytes(KItem)  [function, total]
     syntax Bool ::= definedProjectInt(KItem)  [function, total]
@@ -30,14 +32,18 @@ module CEILS-SYNTAX
         [function, total, klabel(padRightBytesTotal), symbol, no-evaluators]
     syntax Int ::= Int "modIntTotal" Int
         [function, total, klabel(modIntTotal), symbol, no-evaluators, smt-hook(mod)]
+    syntax Int ::= Int "divIntTotal" Int
+        [function, total, klabel(divIntTotal), symbol, no-evaluators, smt-hook(div)]
     syntax Int ::= Int "<<IntTotal" Int
         [function, total, klabel(shlIntTotal), symbol, no-evaluators]
     syntax Int ::= Int ">>IntTotal" Int
         [function, total, klabel(shrIntTotal), symbol, no-evaluators]
     syntax Int ::= Int "^IntTotal" Int
         [function, total, klabel(powIntTotal), symbol, no-evaluators]
+    syntax Int ::= Int "%IntTotal" Int
+        [function, total, klabel(tModIntTotal), symbol, no-evaluators, smtlib(tModInt)]
     syntax Int ::= Int "/IntTotal" Int
-        [function, total, klabel(divIntTotal), symbol, no-evaluators, smt-hook(div)]
+        [function, total, klabel(tDivIntTotal), symbol, no-evaluators, smtlib(tDivInt)]
     syntax Int ::= log2IntTotal(Int)
         [ function, total, klabel(log2IntTotal), symbol, no-evaluators,
           smtlib(log2IntTotal)
diff --git a/kmxwasm/k-src/ceils.k b/kmxwasm/k-src/ceils.k
index 57fc9adc..ab712302 100644
--- a/kmxwasm/k-src/ceils.k
+++ b/kmxwasm/k-src/ceils.k
@@ -141,15 +141,33 @@ module CEILS
         requires definedModInt(Arg0, Arg1)
         [symbolic(Arg1), simplification]
 
-    // rule Arg0:Int modInt Arg1:Int
-    //     => normalizeModIntTotalHelper(Arg0, Arg1) modIntTotal Arg1 // Arg0 modIntTotal Arg1
-    //     requires definedModInt(Arg0, Arg1)
-    //     [symbolic(Arg0), simplification]
+    //----------------------------------
+
+
+    rule definedDivInt (_:Int, X:Int) => X =/=Int 0
+
+    rule #Ceil(@Arg0:Int divInt @Arg1:Int)
+        =>  (({ definedDivInt(@Arg0, @Arg1)  #Equals true }
+          #And #Ceil(@Arg0))
+          #And #Ceil(@Arg1))
+        [simplification]
+
+    rule _ divIntTotal 0 => 0
+
+    rule Arg0:Int divIntTotal Arg1:Int
+        => Arg0 divInt Arg1
+        requires definedDivInt(Arg0, Arg1)
+        [concrete, simplification]
+
+    rule Arg0:Int divInt Arg1:Int
+        => Arg0 divIntTotal Arg1
+        requires definedDivInt(Arg0, Arg1)
+        [symbolic(Arg0), simplification]
 
-    // rule Arg0:Int modInt Arg1:Int
-    //     => normalizeModIntTotalHelper(Arg0, Arg1) modIntTotal Arg1 // Arg0 modIntTotal Arg1
-    //     requires definedModInt(Arg0, Arg1)
-    //     [symbolic(Arg1), simplification]
+    rule Arg0:Int divInt Arg1:Int
+        => Arg0 divIntTotal Arg1
+        requires definedDivInt(Arg0, Arg1)
+        [symbolic(Arg1), simplification]
 
     //----------------------------------
 
@@ -220,27 +238,54 @@ module CEILS
     //-------------------------------------
 
 
-    rule definedDivInt(_:Int, Y:Int) => Y =/=Int 0
+    rule definedTModInt(_:Int, Y:Int) => Y =/=Int 0
+
+    rule #Ceil(@Arg0:Int %Int @Arg1:Int)
+        =>  (({ definedTModInt(@Arg0, @Arg1)  #Equals true }
+          #And #Ceil(@Arg0))
+          #And #Ceil(@Arg1))
+        [simplification]
+
+    rule Arg0:Int %IntTotal Arg1:Int
+        => Arg0 %Int Arg1
+        requires definedTModInt(Arg0, Arg1)
+        [concrete, simplification]
+
+    rule Arg0:Int %Int Arg1:Int
+        => Arg0 %IntTotal Arg1
+        requires definedTModInt(Arg0, Arg1)
+        [symbolic(Arg0), simplification]
+
+    rule Arg0:Int %Int Arg1:Int
+        => Arg0 %IntTotal Arg1
+        requires definedTModInt(Arg0, Arg1)
+        [symbolic(Arg1), simplification]
+
+
+    //-------------------------------------
+
+
+    rule definedTDivInt(_:Int, Y:Int) => Y =/=Int 0
 
     rule #Ceil(@Arg0:Int /Int @Arg1:Int)
-        =>  (({ definedDivInt(@Arg0, @Arg1)  #Equals true }
+        =>  (({ definedTDivInt(@Arg0, @Arg1)  #Equals true }
           #And #Ceil(@Arg0))
           #And #Ceil(@Arg1))
         [simplification]
 
     rule Arg0:Int /IntTotal Arg1:Int
         => Arg0 /Int Arg1
-        requires definedDivInt(Arg0, Arg1)
+        requires definedTDivInt(Arg0, Arg1)
         [concrete, simplification]
 
     rule Arg0:Int /Int Arg1:Int
         => Arg0 /IntTotal Arg1
-        requires definedDivInt(Arg0, Arg1)
+        requires definedTDivInt(Arg0, Arg1)
         [symbolic(Arg0), simplification]
 
     rule Arg0:Int /Int Arg1:Int
         => Arg0 /IntTotal Arg1
-        requires definedDivInt(Arg0, Arg1)
+        requires definedTDivInt(Arg0, Arg1)
         [symbolic(Arg1), simplification]
 
 
@@ -389,4 +434,11 @@ module CEILS
           #And #Ceil(@N)
           [simplification]
 
+    // -----------------------------------
+    // Other stuff
+    // -----------------------------------
+
+    rule I /IntTotal J => I divIntTotal J requires 0 <Int J
+    rule I %IntTotal J => I modIntTotal J requires 0 <Int J
+
 endmodule
diff --git a/kmxwasm/k-src/elrond-lemmas.md b/kmxwasm/k-src/elrond-lemmas.md
index f8b1f32a..321e23f3 100644
--- a/kmxwasm/k-src/elrond-lemmas.md
+++ b/kmxwasm/k-src/elrond-lemmas.md
@@ -8,7 +8,8 @@ module ELROND-LEMMAS
   imports private SET
   imports private WASM-TEXT
 
-  rule size(_:List) >=Int 0 => true  [simplification, smt-lemma]
+  rule  ( size ( _L:List ) >=Int 0 => true )
+    [simplification(), smt-lemma()]
 
   rule Bytes2Int(#getBytesRange(_:Bytes, _:Int, N:Int), _:Endianness, _:Signedness) <Int M:Int
         => true
@@ -31,8 +32,8 @@ module ELROND-LEMMAS
       requires 0 <=Int Value
       [simplification]
 
-  rule { b"" #Equals Int2Bytes(Len:Int, _Value:Int, _:Endianness)} => #Bottom
-      requires Len >Int 0
+  rule { b"" #Equals Int2Bytes(Len:Int, _Value:Int, _E:Endianness)}:Bool
+      => {0 #Equals Len}
       [simplification]
 
   rule 0 <=Int A +Int B => true
@@ -308,8 +309,23 @@ module ELROND-LEMMAS
       requires B =/=Int 0
       [simplification(50)]
 
-  rule A:Int <Int 2 ^IntTotal ((( log2IntTotal(A) +Int 8) /IntTotal 8) *Int 8)
+  // log2IntTotal(X) is the index of the highest bit. This means that
+  // X < 2^(log2IntTotal(X) + 1) since the highest bit of the right term
+  // has a higher index.
+  // We need
+  // 2^(log2IntTotal(X) + 1) <= 2 ^IntTotal (((log2IntTotal(X) +Int 8) divIntTotal 8) *Int 8)
+  // which is equivalent to
+  // log2IntTotal(X) + 1 <= ((log2IntTotal(X) +Int 8) divIntTotal 8) *Int 8.
+  // Let us denote log2IntTotal(X) by Y >= 0
+  // Y + 1 <= (Y divIntTotal 8 + 1) *Int 8.
+  // Y + 1 <= (Y divIntTotal 8) *Int 8 + 8.
+  // Y <= (Y divIntTotal 8) *Int 8 + 7.
+  // Let A be Y divIntTotal 8
+  // Let B be Y modIntTotal 8.
+  // A * 8 + B <= A * 8 + 7, which is obviously true.
+  rule A:Int <Int 2 ^IntTotal ((( log2IntTotal(A) +Int 8) divIntTotal 8) *Int 8)
       => true
+      requires 0 <Int A
       [simplification]
 
   rule  0 <=Int #bool ( _B ) => true
@@ -327,12 +343,6 @@ module ELROND-LEMMAS
   rule  { 1 #Equals #bool ( B:Bool ) } => { true #Equals B:Bool }
     [simplification()]
 
-  rule  X:Int <=Int maxInt ( Y:Int , Z:Int ) => true
-    requires ( X:Int <=Int Y:Int
-      orBool ( X:Int <=Int Z:Int
-              ))
-    [simplification()]
-
   rule  X:Int <Int maxInt ( Y:Int , Z:Int ) => true
     requires ( X:Int <Int Y:Int
       orBool ( X:Int <Int Z:Int
diff --git a/kmxwasm/k-src/elrond-semantics b/kmxwasm/k-src/elrond-semantics
index 58ccff40..1c0c214f 160000
--- a/kmxwasm/k-src/elrond-semantics
+++ b/kmxwasm/k-src/elrond-semantics
@@ -1 +1 @@
-Subproject commit 58ccff40b06f6f19791ec3494d6c51ad21fd858f
+Subproject commit 1c0c214f82c03407559983b4f0da58d2dc91b04c
diff --git a/kmxwasm/k-src/specification-lemmas.md b/kmxwasm/k-src/specification-lemmas.md
index a3648978..3d7f91fe 100644
--- a/kmxwasm/k-src/specification-lemmas.md
+++ b/kmxwasm/k-src/specification-lemmas.md
@@ -1,5 +1,6 @@
 ```k
 module SPECIFICATION-LEMMAS
+    imports private CEILS-SYNTAX
     imports private INT
     imports private LIST
 
@@ -16,5 +17,26 @@ module SPECIFICATION-LEMMAS
     rule minInt(A:Int, B:Int) => A requires A <=Int B
         [simplification]
 
+    // Y > 0
+    rule X /IntTotal Y => 0
+        requires 0 <=Int X andBool X <Int Y
+        [simplification]
+    rule X /IntTotal Y => 1 +Int ((X -Int Y) /IntTotal Y)
+        requires 0 <Int Y andBool Y <=Int X
+        [simplification]
+    rule X /IntTotal Y => ((X +Int Y) /IntTotal Y) -Int 1
+        requires 0 <Int Y andBool X <Int 0
+        [simplification]
+    // Y < 0
+    rule X /IntTotal Y => 0
+        requires Y <Int X andBool X <=Int 0
+        [simplification]
+    rule X /IntTotal Y => 1 +Int ((X -Int Y) /IntTotal Y)
+        requires X <=Int Y andBool Y <Int 0
+        [simplification]
+    rule X /IntTotal Y => ((X +Int Y) /IntTotal Y) -Int 1
+        requires Y <Int 0 andBool 0 <Int X
+        [simplification]
+
 endmodule
 ```
\ No newline at end of file
diff --git a/kmxwasm/poetry.lock b/kmxwasm/poetry.lock
index 8b346812..eb9c9383 100644
--- a/kmxwasm/poetry.lock
+++ b/kmxwasm/poetry.lock
@@ -20,13 +20,13 @@ tests-no-zope = ["cloudpickle", "hypothesis", "mypy (>=1.1.1)", "pympler", "pyte
 
 [[package]]
 name = "autoflake"
-version = "2.2.0"
+version = "2.2.1"
 description = "Removes unused imports and unused variables"
 optional = false
 python-versions = ">=3.8"
 files = [
-    {file = "autoflake-2.2.0-py3-none-any.whl", hash = "sha256:de409b009a34c1c2a7cc2aae84c4c05047f9773594317c6a6968bd497600d4a0"},
-    {file = "autoflake-2.2.0.tar.gz", hash = "sha256:62e1f74a0fdad898a96fee6f99fe8241af90ad99c7110c884b35855778412251"},
+    {file = "autoflake-2.2.1-py3-none-any.whl", hash = "sha256:265cde0a43c1f44ecfb4f30d95b0437796759d07be7706a2f70e4719234c0f79"},
+    {file = "autoflake-2.2.1.tar.gz", hash = "sha256:62b7b6449a692c3c9b0c916919bbc21648da7281e8506bcf8d3f8280e431ebc1"},
 ]
 
 [package.dependencies]
@@ -35,33 +35,33 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""}
 
 [[package]]
 name = "black"
-version = "23.7.0"
+version = "23.9.1"
 description = "The uncompromising code formatter."
 optional = false
 python-versions = ">=3.8"
 files = [
-    {file = "black-23.7.0-cp310-cp310-macosx_10_16_arm64.whl", hash = "sha256:5c4bc552ab52f6c1c506ccae05681fab58c3f72d59ae6e6639e8885e94fe2587"},
-    {file = "black-23.7.0-cp310-cp310-macosx_10_16_universal2.whl", hash = "sha256:552513d5cd5694590d7ef6f46e1767a4df9af168d449ff767b13b084c020e63f"},
-    {file = "black-23.7.0-cp310-cp310-macosx_10_16_x86_64.whl", hash = "sha256:86cee259349b4448adb4ef9b204bb4467aae74a386bce85d56ba4f5dc0da27be"},
-    {file = "black-23.7.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:501387a9edcb75d7ae8a4412bb8749900386eaef258f1aefab18adddea1936bc"},
-    {file = "black-23.7.0-cp310-cp310-win_amd64.whl", hash = "sha256:fb074d8b213749fa1d077d630db0d5f8cc3b2ae63587ad4116e8a436e9bbe995"},
-    {file = "black-23.7.0-cp311-cp311-macosx_10_16_arm64.whl", hash = "sha256:b5b0ee6d96b345a8b420100b7d71ebfdd19fab5e8301aff48ec270042cd40ac2"},
-    {file = "black-23.7.0-cp311-cp311-macosx_10_16_universal2.whl", hash = "sha256:893695a76b140881531062d48476ebe4a48f5d1e9388177e175d76234ca247cd"},
-    {file = "black-23.7.0-cp311-cp311-macosx_10_16_x86_64.whl", hash = "sha256:c333286dc3ddca6fdff74670b911cccedacb4ef0a60b34e491b8a67c833b343a"},
-    {file = "black-23.7.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:831d8f54c3a8c8cf55f64d0422ee875eecac26f5f649fb6c1df65316b67c8926"},
-    {file = "black-23.7.0-cp311-cp311-win_amd64.whl", hash = "sha256:7f3bf2dec7d541b4619b8ce526bda74a6b0bffc480a163fed32eb8b3c9aed8ad"},
-    {file = "black-23.7.0-cp38-cp38-macosx_10_16_arm64.whl", hash = "sha256:f9062af71c59c004cd519e2fb8f5d25d39e46d3af011b41ab43b9c74e27e236f"},
-    {file = "black-23.7.0-cp38-cp38-macosx_10_16_universal2.whl", hash = "sha256:01ede61aac8c154b55f35301fac3e730baf0c9cf8120f65a9cd61a81cfb4a0c3"},
-    {file = "black-23.7.0-cp38-cp38-macosx_10_16_x86_64.whl", hash = "sha256:327a8c2550ddc573b51e2c352adb88143464bb9d92c10416feb86b0f5aee5ff6"},
-    {file = "black-23.7.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6d1c6022b86f83b632d06f2b02774134def5d4d4f1dac8bef16d90cda18ba28a"},
-    {file = "black-23.7.0-cp38-cp38-win_amd64.whl", hash = "sha256:27eb7a0c71604d5de083757fbdb245b1a4fae60e9596514c6ec497eb63f95320"},
-    {file = "black-23.7.0-cp39-cp39-macosx_10_16_arm64.whl", hash = "sha256:8417dbd2f57b5701492cd46edcecc4f9208dc75529bcf76c514864e48da867d9"},
-    {file = "black-23.7.0-cp39-cp39-macosx_10_16_universal2.whl", hash = "sha256:47e56d83aad53ca140da0af87678fb38e44fd6bc0af71eebab2d1f59b1acf1d3"},
-    {file = "black-23.7.0-cp39-cp39-macosx_10_16_x86_64.whl", hash = "sha256:25cc308838fe71f7065df53aedd20327969d05671bac95b38fdf37ebe70ac087"},
-    {file = "black-23.7.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:642496b675095d423f9b8448243336f8ec71c9d4d57ec17bf795b67f08132a91"},
-    {file = "black-23.7.0-cp39-cp39-win_amd64.whl", hash = "sha256:ad0014efc7acf0bd745792bd0d8857413652979200ab924fbf239062adc12491"},
-    {file = "black-23.7.0-py3-none-any.whl", hash = "sha256:9fd59d418c60c0348505f2ddf9609c1e1de8e7493eab96198fc89d9f865e7a96"},
-    {file = "black-23.7.0.tar.gz", hash = "sha256:022a582720b0d9480ed82576c920a8c1dde97cc38ff11d8d8859b3bd6ca9eedb"},
+    {file = "black-23.9.1-cp310-cp310-macosx_10_16_arm64.whl", hash = "sha256:d6bc09188020c9ac2555a498949401ab35bb6bf76d4e0f8ee251694664df6301"},
+    {file = "black-23.9.1-cp310-cp310-macosx_10_16_universal2.whl", hash = "sha256:13ef033794029b85dfea8032c9d3b92b42b526f1ff4bf13b2182ce4e917f5100"},
+    {file = "black-23.9.1-cp310-cp310-macosx_10_16_x86_64.whl", hash = "sha256:75a2dc41b183d4872d3a500d2b9c9016e67ed95738a3624f4751a0cb4818fe71"},
+    {file = "black-23.9.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:13a2e4a93bb8ca74a749b6974925c27219bb3df4d42fc45e948a5d9feb5122b7"},
+    {file = "black-23.9.1-cp310-cp310-win_amd64.whl", hash = "sha256:adc3e4442eef57f99b5590b245a328aad19c99552e0bdc7f0b04db6656debd80"},
+    {file = "black-23.9.1-cp311-cp311-macosx_10_16_arm64.whl", hash = "sha256:8431445bf62d2a914b541da7ab3e2b4f3bc052d2ccbf157ebad18ea126efb91f"},
+    {file = "black-23.9.1-cp311-cp311-macosx_10_16_universal2.whl", hash = "sha256:8fc1ddcf83f996247505db6b715294eba56ea9372e107fd54963c7553f2b6dfe"},
+    {file = "black-23.9.1-cp311-cp311-macosx_10_16_x86_64.whl", hash = "sha256:7d30ec46de88091e4316b17ae58bbbfc12b2de05e069030f6b747dfc649ad186"},
+    {file = "black-23.9.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:031e8c69f3d3b09e1aa471a926a1eeb0b9071f80b17689a655f7885ac9325a6f"},
+    {file = "black-23.9.1-cp311-cp311-win_amd64.whl", hash = "sha256:538efb451cd50f43aba394e9ec7ad55a37598faae3348d723b59ea8e91616300"},
+    {file = "black-23.9.1-cp38-cp38-macosx_10_16_arm64.whl", hash = "sha256:638619a559280de0c2aa4d76f504891c9860bb8fa214267358f0a20f27c12948"},
+    {file = "black-23.9.1-cp38-cp38-macosx_10_16_universal2.whl", hash = "sha256:a732b82747235e0542c03bf352c126052c0fbc458d8a239a94701175b17d4855"},
+    {file = "black-23.9.1-cp38-cp38-macosx_10_16_x86_64.whl", hash = "sha256:cf3a4d00e4cdb6734b64bf23cd4341421e8953615cba6b3670453737a72ec204"},
+    {file = "black-23.9.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:cf99f3de8b3273a8317681d8194ea222f10e0133a24a7548c73ce44ea1679377"},
+    {file = "black-23.9.1-cp38-cp38-win_amd64.whl", hash = "sha256:14f04c990259576acd093871e7e9b14918eb28f1866f91968ff5524293f9c573"},
+    {file = "black-23.9.1-cp39-cp39-macosx_10_16_arm64.whl", hash = "sha256:c619f063c2d68f19b2d7270f4cf3192cb81c9ec5bc5ba02df91471d0b88c4c5c"},
+    {file = "black-23.9.1-cp39-cp39-macosx_10_16_universal2.whl", hash = "sha256:6a3b50e4b93f43b34a9d3ef00d9b6728b4a722c997c99ab09102fd5efdb88325"},
+    {file = "black-23.9.1-cp39-cp39-macosx_10_16_x86_64.whl", hash = "sha256:c46767e8df1b7beefb0899c4a95fb43058fa8500b6db144f4ff3ca38eb2f6393"},
+    {file = "black-23.9.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:50254ebfa56aa46a9fdd5d651f9637485068a1adf42270148cd101cdf56e0ad9"},
+    {file = "black-23.9.1-cp39-cp39-win_amd64.whl", hash = "sha256:403397c033adbc45c2bd41747da1f7fc7eaa44efbee256b53842470d4ac5a70f"},
+    {file = "black-23.9.1-py3-none-any.whl", hash = "sha256:6ccd59584cc834b6d127628713e4b6b968e5f79572da66284532525a042549f9"},
+    {file = "black-23.9.1.tar.gz", hash = "sha256:24b6b3ff5c6d9ea08a8888f6977eae858e1f340d7260cf56d70a49823236b62d"},
 ]
 
 [package.dependencies]
@@ -71,6 +71,7 @@ packaging = ">=22.0"
 pathspec = ">=0.9.0"
 platformdirs = ">=2"
 tomli = {version = ">=1.1.0", markers = "python_version < \"3.11\""}
+typing-extensions = {version = ">=4.0.1", markers = "python_version < \"3.11\""}
 
 [package.extras]
 colorama = ["colorama (>=0.4.3)"]
@@ -144,63 +145,63 @@ cron = ["capturer (>=2.4)"]
 
 [[package]]
 name = "coverage"
-version = "7.3.0"
+version = "7.3.1"
 description = "Code coverage measurement for Python"
 optional = false
 python-versions = ">=3.8"
 files = [
-    {file = "coverage-7.3.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:db76a1bcb51f02b2007adacbed4c88b6dee75342c37b05d1822815eed19edee5"},
-    {file = "coverage-7.3.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:c02cfa6c36144ab334d556989406837336c1d05215a9bdf44c0bc1d1ac1cb637"},
-    {file = "coverage-7.3.0-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:477c9430ad5d1b80b07f3c12f7120eef40bfbf849e9e7859e53b9c93b922d2af"},
-    {file = "coverage-7.3.0-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ce2ee86ca75f9f96072295c5ebb4ef2a43cecf2870b0ca5e7a1cbdd929cf67e1"},
-    {file = "coverage-7.3.0-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:68d8a0426b49c053013e631c0cdc09b952d857efa8f68121746b339912d27a12"},
-    {file = "coverage-7.3.0-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:b3eb0c93e2ea6445b2173da48cb548364f8f65bf68f3d090404080d338e3a689"},
-    {file = "coverage-7.3.0-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:90b6e2f0f66750c5a1178ffa9370dec6c508a8ca5265c42fbad3ccac210a7977"},
-    {file = "coverage-7.3.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:96d7d761aea65b291a98c84e1250cd57b5b51726821a6f2f8df65db89363be51"},
-    {file = "coverage-7.3.0-cp310-cp310-win32.whl", hash = "sha256:63c5b8ecbc3b3d5eb3a9d873dec60afc0cd5ff9d9f1c75981d8c31cfe4df8527"},
-    {file = "coverage-7.3.0-cp310-cp310-win_amd64.whl", hash = "sha256:97c44f4ee13bce914272589b6b41165bbb650e48fdb7bd5493a38bde8de730a1"},
-    {file = "coverage-7.3.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:74c160285f2dfe0acf0f72d425f3e970b21b6de04157fc65adc9fd07ee44177f"},
-    {file = "coverage-7.3.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:b543302a3707245d454fc49b8ecd2c2d5982b50eb63f3535244fd79a4be0c99d"},
-    {file = "coverage-7.3.0-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ad0f87826c4ebd3ef484502e79b39614e9c03a5d1510cfb623f4a4a051edc6fd"},
-    {file = "coverage-7.3.0-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:13c6cbbd5f31211d8fdb477f0f7b03438591bdd077054076eec362cf2207b4a7"},
-    {file = "coverage-7.3.0-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fac440c43e9b479d1241fe9d768645e7ccec3fb65dc3a5f6e90675e75c3f3e3a"},
-    {file = "coverage-7.3.0-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:3c9834d5e3df9d2aba0275c9f67989c590e05732439b3318fa37a725dff51e74"},
-    {file = "coverage-7.3.0-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:4c8e31cf29b60859876474034a83f59a14381af50cbe8a9dbaadbf70adc4b214"},
-    {file = "coverage-7.3.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:7a9baf8e230f9621f8e1d00c580394a0aa328fdac0df2b3f8384387c44083c0f"},
-    {file = "coverage-7.3.0-cp311-cp311-win32.whl", hash = "sha256:ccc51713b5581e12f93ccb9c5e39e8b5d4b16776d584c0f5e9e4e63381356482"},
-    {file = "coverage-7.3.0-cp311-cp311-win_amd64.whl", hash = "sha256:887665f00ea4e488501ba755a0e3c2cfd6278e846ada3185f42d391ef95e7e70"},
-    {file = "coverage-7.3.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:d000a739f9feed900381605a12a61f7aaced6beae832719ae0d15058a1e81c1b"},
-    {file = "coverage-7.3.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:59777652e245bb1e300e620ce2bef0d341945842e4eb888c23a7f1d9e143c446"},
-    {file = "coverage-7.3.0-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c9737bc49a9255d78da085fa04f628a310c2332b187cd49b958b0e494c125071"},
-    {file = "coverage-7.3.0-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:5247bab12f84a1d608213b96b8af0cbb30d090d705b6663ad794c2f2a5e5b9fe"},
-    {file = "coverage-7.3.0-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e2ac9a1de294773b9fa77447ab7e529cf4fe3910f6a0832816e5f3d538cfea9a"},
-    {file = "coverage-7.3.0-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:85b7335c22455ec12444cec0d600533a238d6439d8d709d545158c1208483873"},
-    {file = "coverage-7.3.0-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:36ce5d43a072a036f287029a55b5c6a0e9bd73db58961a273b6dc11a2c6eb9c2"},
-    {file = "coverage-7.3.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:211a4576e984f96d9fce61766ffaed0115d5dab1419e4f63d6992b480c2bd60b"},
-    {file = "coverage-7.3.0-cp312-cp312-win32.whl", hash = "sha256:56afbf41fa4a7b27f6635bc4289050ac3ab7951b8a821bca46f5b024500e6321"},
-    {file = "coverage-7.3.0-cp312-cp312-win_amd64.whl", hash = "sha256:7f297e0c1ae55300ff688568b04ff26b01c13dfbf4c9d2b7d0cb688ac60df479"},
-    {file = "coverage-7.3.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:ac0dec90e7de0087d3d95fa0533e1d2d722dcc008bc7b60e1143402a04c117c1"},
-    {file = "coverage-7.3.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:438856d3f8f1e27f8e79b5410ae56650732a0dcfa94e756df88c7e2d24851fcd"},
-    {file = "coverage-7.3.0-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1084393c6bda8875c05e04fce5cfe1301a425f758eb012f010eab586f1f3905e"},
-    {file = "coverage-7.3.0-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:49ab200acf891e3dde19e5aa4b0f35d12d8b4bd805dc0be8792270c71bd56c54"},
-    {file = "coverage-7.3.0-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a67e6bbe756ed458646e1ef2b0778591ed4d1fcd4b146fc3ba2feb1a7afd4254"},
-    {file = "coverage-7.3.0-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:8f39c49faf5344af36042b293ce05c0d9004270d811c7080610b3e713251c9b0"},
-    {file = "coverage-7.3.0-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:7df91fb24c2edaabec4e0eee512ff3bc6ec20eb8dccac2e77001c1fe516c0c84"},
-    {file = "coverage-7.3.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:34f9f0763d5fa3035a315b69b428fe9c34d4fc2f615262d6be3d3bf3882fb985"},
-    {file = "coverage-7.3.0-cp38-cp38-win32.whl", hash = "sha256:bac329371d4c0d456e8d5f38a9b0816b446581b5f278474e416ea0c68c47dcd9"},
-    {file = "coverage-7.3.0-cp38-cp38-win_amd64.whl", hash = "sha256:b859128a093f135b556b4765658d5d2e758e1fae3e7cc2f8c10f26fe7005e543"},
-    {file = "coverage-7.3.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:fc0ed8d310afe013db1eedd37176d0839dc66c96bcfcce8f6607a73ffea2d6ba"},
-    {file = "coverage-7.3.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:e61260ec93f99f2c2d93d264b564ba912bec502f679793c56f678ba5251f0393"},
-    {file = "coverage-7.3.0-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:97af9554a799bd7c58c0179cc8dbf14aa7ab50e1fd5fa73f90b9b7215874ba28"},
-    {file = "coverage-7.3.0-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:3558e5b574d62f9c46b76120a5c7c16c4612dc2644c3d48a9f4064a705eaee95"},
-    {file = "coverage-7.3.0-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:37d5576d35fcb765fca05654f66aa71e2808d4237d026e64ac8b397ffa66a56a"},
-    {file = "coverage-7.3.0-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:07ea61bcb179f8f05ffd804d2732b09d23a1238642bf7e51dad62082b5019b34"},
-    {file = "coverage-7.3.0-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:80501d1b2270d7e8daf1b64b895745c3e234289e00d5f0e30923e706f110334e"},
-    {file = "coverage-7.3.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:4eddd3153d02204f22aef0825409091a91bf2a20bce06fe0f638f5c19a85de54"},
-    {file = "coverage-7.3.0-cp39-cp39-win32.whl", hash = "sha256:2d22172f938455c156e9af2612650f26cceea47dc86ca048fa4e0b2d21646ad3"},
-    {file = "coverage-7.3.0-cp39-cp39-win_amd64.whl", hash = "sha256:60f64e2007c9144375dd0f480a54d6070f00bb1a28f65c408370544091c9bc9e"},
-    {file = "coverage-7.3.0-pp38.pp39.pp310-none-any.whl", hash = "sha256:5492a6ce3bdb15c6ad66cb68a0244854d9917478877a25671d70378bdc8562d0"},
-    {file = "coverage-7.3.0.tar.gz", hash = "sha256:49dbb19cdcafc130f597d9e04a29d0a032ceedf729e41b181f51cd170e6ee865"},
+    {file = "coverage-7.3.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:cd0f7429ecfd1ff597389907045ff209c8fdb5b013d38cfa7c60728cb484b6e3"},
+    {file = "coverage-7.3.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:966f10df9b2b2115da87f50f6a248e313c72a668248be1b9060ce935c871f276"},
+    {file = "coverage-7.3.1-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:0575c37e207bb9b98b6cf72fdaaa18ac909fb3d153083400c2d48e2e6d28bd8e"},
+    {file = "coverage-7.3.1-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:245c5a99254e83875c7fed8b8b2536f040997a9b76ac4c1da5bff398c06e860f"},
+    {file = "coverage-7.3.1-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4c96dd7798d83b960afc6c1feb9e5af537fc4908852ef025600374ff1a017392"},
+    {file = "coverage-7.3.1-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:de30c1aa80f30af0f6b2058a91505ea6e36d6535d437520067f525f7df123887"},
+    {file = "coverage-7.3.1-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:50dd1e2dd13dbbd856ffef69196781edff26c800a74f070d3b3e3389cab2600d"},
+    {file = "coverage-7.3.1-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:b9c0c19f70d30219113b18fe07e372b244fb2a773d4afde29d5a2f7930765136"},
+    {file = "coverage-7.3.1-cp310-cp310-win32.whl", hash = "sha256:770f143980cc16eb601ccfd571846e89a5fe4c03b4193f2e485268f224ab602f"},
+    {file = "coverage-7.3.1-cp310-cp310-win_amd64.whl", hash = "sha256:cdd088c00c39a27cfa5329349cc763a48761fdc785879220d54eb785c8a38520"},
+    {file = "coverage-7.3.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:74bb470399dc1989b535cb41f5ca7ab2af561e40def22d7e188e0a445e7639e3"},
+    {file = "coverage-7.3.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:025ded371f1ca280c035d91b43252adbb04d2aea4c7105252d3cbc227f03b375"},
+    {file = "coverage-7.3.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a6191b3a6ad3e09b6cfd75b45c6aeeffe7e3b0ad46b268345d159b8df8d835f9"},
+    {file = "coverage-7.3.1-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:7eb0b188f30e41ddd659a529e385470aa6782f3b412f860ce22b2491c89b8593"},
+    {file = "coverage-7.3.1-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:75c8f0df9dfd8ff745bccff75867d63ef336e57cc22b2908ee725cc552689ec8"},
+    {file = "coverage-7.3.1-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:7eb3cd48d54b9bd0e73026dedce44773214064be93611deab0b6a43158c3d5a0"},
+    {file = "coverage-7.3.1-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:ac3c5b7e75acac31e490b7851595212ed951889918d398b7afa12736c85e13ce"},
+    {file = "coverage-7.3.1-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:5b4ee7080878077af0afa7238df1b967f00dc10763f6e1b66f5cced4abebb0a3"},
+    {file = "coverage-7.3.1-cp311-cp311-win32.whl", hash = "sha256:229c0dd2ccf956bf5aeede7e3131ca48b65beacde2029f0361b54bf93d36f45a"},
+    {file = "coverage-7.3.1-cp311-cp311-win_amd64.whl", hash = "sha256:c6f55d38818ca9596dc9019eae19a47410d5322408140d9a0076001a3dcb938c"},
+    {file = "coverage-7.3.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:5289490dd1c3bb86de4730a92261ae66ea8d44b79ed3cc26464f4c2cde581fbc"},
+    {file = "coverage-7.3.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:ca833941ec701fda15414be400c3259479bfde7ae6d806b69e63b3dc423b1832"},
+    {file = "coverage-7.3.1-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:cd694e19c031733e446c8024dedd12a00cda87e1c10bd7b8539a87963685e969"},
+    {file = "coverage-7.3.1-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:aab8e9464c00da5cb9c536150b7fbcd8850d376d1151741dd0d16dfe1ba4fd26"},
+    {file = "coverage-7.3.1-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:87d38444efffd5b056fcc026c1e8d862191881143c3aa80bb11fcf9dca9ae204"},
+    {file = "coverage-7.3.1-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:8a07b692129b8a14ad7a37941a3029c291254feb7a4237f245cfae2de78de037"},
+    {file = "coverage-7.3.1-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:2829c65c8faaf55b868ed7af3c7477b76b1c6ebeee99a28f59a2cb5907a45760"},
+    {file = "coverage-7.3.1-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:1f111a7d85658ea52ffad7084088277135ec5f368457275fc57f11cebb15607f"},
+    {file = "coverage-7.3.1-cp312-cp312-win32.whl", hash = "sha256:c397c70cd20f6df7d2a52283857af622d5f23300c4ca8e5bd8c7a543825baa5a"},
+    {file = "coverage-7.3.1-cp312-cp312-win_amd64.whl", hash = "sha256:5ae4c6da8b3d123500f9525b50bf0168023313963e0e2e814badf9000dd6ef92"},
+    {file = "coverage-7.3.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:ca70466ca3a17460e8fc9cea7123c8cbef5ada4be3140a1ef8f7b63f2f37108f"},
+    {file = "coverage-7.3.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:f2781fd3cabc28278dc982a352f50c81c09a1a500cc2086dc4249853ea96b981"},
+    {file = "coverage-7.3.1-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6407424621f40205bbe6325686417e5e552f6b2dba3535dd1f90afc88a61d465"},
+    {file = "coverage-7.3.1-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:04312b036580ec505f2b77cbbdfb15137d5efdfade09156961f5277149f5e344"},
+    {file = "coverage-7.3.1-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ac9ad38204887349853d7c313f53a7b1c210ce138c73859e925bc4e5d8fc18e7"},
+    {file = "coverage-7.3.1-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:53669b79f3d599da95a0afbef039ac0fadbb236532feb042c534fbb81b1a4e40"},
+    {file = "coverage-7.3.1-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:614f1f98b84eb256e4f35e726bfe5ca82349f8dfa576faabf8a49ca09e630086"},
+    {file = "coverage-7.3.1-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:f1a317fdf5c122ad642db8a97964733ab7c3cf6009e1a8ae8821089993f175ff"},
+    {file = "coverage-7.3.1-cp38-cp38-win32.whl", hash = "sha256:defbbb51121189722420a208957e26e49809feafca6afeef325df66c39c4fdb3"},
+    {file = "coverage-7.3.1-cp38-cp38-win_amd64.whl", hash = "sha256:f4f456590eefb6e1b3c9ea6328c1e9fa0f1006e7481179d749b3376fc793478e"},
+    {file = "coverage-7.3.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:f12d8b11a54f32688b165fd1a788c408f927b0960984b899be7e4c190ae758f1"},
+    {file = "coverage-7.3.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:f09195dda68d94a53123883de75bb97b0e35f5f6f9f3aa5bf6e496da718f0cb6"},
+    {file = "coverage-7.3.1-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c6601a60318f9c3945be6ea0f2a80571f4299b6801716f8a6e4846892737ebe4"},
+    {file = "coverage-7.3.1-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:07d156269718670d00a3b06db2288b48527fc5f36859425ff7cec07c6b367745"},
+    {file = "coverage-7.3.1-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:636a8ac0b044cfeccae76a36f3b18264edcc810a76a49884b96dd744613ec0b7"},
+    {file = "coverage-7.3.1-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:5d991e13ad2ed3aced177f524e4d670f304c8233edad3210e02c465351f785a0"},
+    {file = "coverage-7.3.1-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:586649ada7cf139445da386ab6f8ef00e6172f11a939fc3b2b7e7c9082052fa0"},
+    {file = "coverage-7.3.1-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:4aba512a15a3e1e4fdbfed2f5392ec221434a614cc68100ca99dcad7af29f3f8"},
+    {file = "coverage-7.3.1-cp39-cp39-win32.whl", hash = "sha256:6bc6f3f4692d806831c136c5acad5ccedd0262aa44c087c46b7101c77e139140"},
+    {file = "coverage-7.3.1-cp39-cp39-win_amd64.whl", hash = "sha256:553d7094cb27db58ea91332e8b5681bac107e7242c23f7629ab1316ee73c4981"},
+    {file = "coverage-7.3.1-pp38.pp39.pp310-none-any.whl", hash = "sha256:220eb51f5fb38dfdb7e5d54284ca4d0cd70ddac047d750111a68ab1798945194"},
+    {file = "coverage-7.3.1.tar.gz", hash = "sha256:6cb7fe1581deb67b782c153136541e20901aa312ceedaf1467dcb35255787952"},
 ]
 
 [package.dependencies]
@@ -239,18 +240,21 @@ testing = ["hatch", "pre-commit", "pytest", "tox"]
 
 [[package]]
 name = "filelock"
-version = "3.12.2"
+version = "3.12.3"
 description = "A platform independent file lock."
 optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.8"
 files = [
-    {file = "filelock-3.12.2-py3-none-any.whl", hash = "sha256:cbb791cdea2a72f23da6ac5b5269ab0a0d161e9ef0100e653b69049a7706d1ec"},
-    {file = "filelock-3.12.2.tar.gz", hash = "sha256:002740518d8aa59a26b0c76e10fb8c6e15eae825d34b6fdf670333fd7b938d81"},
+    {file = "filelock-3.12.3-py3-none-any.whl", hash = "sha256:f067e40ccc40f2b48395a80fcbd4728262fab54e232e090a4063ab804179efeb"},
+    {file = "filelock-3.12.3.tar.gz", hash = "sha256:0ecc1dd2ec4672a10c8550a8182f1bd0c0a5088470ecd5a125e45f49472fac3d"},
 ]
 
+[package.dependencies]
+typing-extensions = {version = ">=4.7.1", markers = "python_version < \"3.11\""}
+
 [package.extras]
-docs = ["furo (>=2023.5.20)", "sphinx (>=7.0.1)", "sphinx-autodoc-typehints (>=1.23,!=1.23.4)"]
-testing = ["covdefaults (>=2.3)", "coverage (>=7.2.7)", "diff-cover (>=7.5)", "pytest (>=7.3.1)", "pytest-cov (>=4.1)", "pytest-mock (>=3.10)", "pytest-timeout (>=2.1)"]
+docs = ["furo (>=2023.7.26)", "sphinx (>=7.1.2)", "sphinx-autodoc-typehints (>=1.24)"]
+testing = ["covdefaults (>=2.3)", "coverage (>=7.3)", "diff-cover (>=7.7)", "pytest (>=7.4)", "pytest-cov (>=4.1)", "pytest-mock (>=3.11.1)", "pytest-timeout (>=2.1)"]
 
 [[package]]
 name = "flake8"
@@ -587,13 +591,13 @@ test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4)", "pytest-co
 
 [[package]]
 name = "pluggy"
-version = "1.2.0"
+version = "1.3.0"
 description = "plugin and hook calling mechanisms for python"
 optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.8"
 files = [
-    {file = "pluggy-1.2.0-py3-none-any.whl", hash = "sha256:c2fd55a7d7a3863cba1a013e4e2414658b1d07b6bc57b3919e0c63c9abb99849"},
-    {file = "pluggy-1.2.0.tar.gz", hash = "sha256:d12f0c4b579b15f5e054301bb226ee85eeeba08ffec228092f8defbaa3a4c4b3"},
+    {file = "pluggy-1.3.0-py3-none-any.whl", hash = "sha256:d89c696a773f8bd377d18e5ecda92b7a3793cbe66c87060a6fb58c7b6e1061f7"},
+    {file = "pluggy-1.3.0.tar.gz", hash = "sha256:cf61ae8f126ac6f7c451172cf30e3e43d3ca77615509771b3a984a0730651e12"},
 ]
 
 [package.extras]
@@ -678,7 +682,7 @@ plugins = ["importlib-metadata"]
 
 [[package]]
 name = "pyk"
-version = "0.1.417"
+version = "0.1.438"
 description = ""
 optional = false
 python-versions = "^3.10"
@@ -698,8 +702,8 @@ tomli = "^2.0.1"
 [package.source]
 type = "git"
 url = "https://github.com/runtimeverification/pyk.git"
-reference = "v0.1.417"
-resolved_reference = "0151483b7f9174f9c2652fcf5b026ddd87092151"
+reference = "v0.1.438"
+resolved_reference = "16b75f582d32e80c65082e2f25db540b3689d4cc"
 
 [[package]]
 name = "pyperclip"
@@ -724,13 +728,13 @@ files = [
 
 [[package]]
 name = "pytest"
-version = "7.4.0"
+version = "7.4.2"
 description = "pytest: simple powerful testing with Python"
 optional = false
 python-versions = ">=3.7"
 files = [
-    {file = "pytest-7.4.0-py3-none-any.whl", hash = "sha256:78bf16451a2eb8c7a2ea98e32dc119fd2aa758f1d5d66dbf0a59d69a3969df32"},
-    {file = "pytest-7.4.0.tar.gz", hash = "sha256:b4bf8c45bd59934ed84001ad51e11b4ee40d40a1229d2c79f9c592b0a3f6bd8a"},
+    {file = "pytest-7.4.2-py3-none-any.whl", hash = "sha256:1d881c6124e08ff0a1bb75ba3ec0bfd8b5354a01c194ddd5a0a870a48d99b002"},
+    {file = "pytest-7.4.2.tar.gz", hash = "sha256:a766259cfab564a2ad52cb1aae1b881a75c3eb7e34ca3779697c23ed47c47069"},
 ]
 
 [package.dependencies]
@@ -902,4 +906,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p
 [metadata]
 lock-version = "2.0"
 python-versions = "^3.10"
-content-hash = "4c945698c044768c640f8e28ad0c781ee92525d84a60023e923fb1a02b347761"
+content-hash = "0804a5dea6de1e7febc662f354f438bc318085e7d16966294bfce2260e21074b"
diff --git a/kmxwasm/pyproject.toml b/kmxwasm/pyproject.toml
index 8583fcd0..ec252a0b 100644
--- a/kmxwasm/pyproject.toml
+++ b/kmxwasm/pyproject.toml
@@ -12,7 +12,7 @@ authors = [
 
 [tool.poetry.dependencies]
 python = "^3.10"
-pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.417" }
+pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.438" }
 # pyk = { path = "/mnt/data/runtime-verification/pyk", develop = true }
 
 [tool.poetry.group.dev.dependencies]
diff --git a/kmxwasm/src/kmxwasm/ast/elrond.py b/kmxwasm/src/kmxwasm/ast/elrond.py
index 2b0c770e..c6aa4a88 100644
--- a/kmxwasm/src/kmxwasm/ast/elrond.py
+++ b/kmxwasm/src/kmxwasm/ast/elrond.py
@@ -1,8 +1,17 @@
 from typing import Iterable
 
-from pyk.kast.inner import KInner
+from pyk.kast.inner import KApply, KInner, KSequence, collect
 
 from .collections import cell_map, full_list, k_map, simple_list
+from .generic import replace_with_path, set_ksequence_cell_contents, set_single_argument_kapply_contents
+
+COMMANDS_CELL_NAME = '<commands>'
+WASM_CELL_NAME = '<wasm>'
+CONTRACT_MOD_IDX_CELL_NAME = '<contractModIdx>'
+
+CALL_STATE_PATH = ['<foundry>', '<mandos>', '<elrond>', '<node>', '<callState>']
+WASM_CELL_PATH = CALL_STATE_PATH + [WASM_CELL_NAME]
+CONTRACT_MOD_IDX_CELL_PATH = CALL_STATE_PATH + [CONTRACT_MOD_IDX_CELL_NAME]
 
 
 # TODO: Move these to the elrond-semantics repository.
@@ -22,3 +31,95 @@ def bytesStack(items: Iterable[KInner]) -> KInner:  # noqa: N802
 
 def accountCellMap(accounts: Iterable[KInner]) -> KInner:  # noqa: N802
     return cell_map(name='AccountCellMap', items=accounts)
+
+
+def find_single_named_node(root: KInner, name: str) -> KApply:
+    nodes: list[KApply] = []
+
+    def commands_cell(node: KInner) -> None:
+        if not isinstance(node, KApply):
+            return
+        if node.label.name == name:
+            nodes.append(node)
+
+    collect(commands_cell, root)
+    assert len(nodes) == 1
+    return nodes[0]
+
+
+def get_commands_cell(root: KInner) -> KApply:
+    return find_single_named_node(root, COMMANDS_CELL_NAME)
+
+
+def commands_cell_contents(root: KInner) -> KSequence:
+    commands = get_commands_cell(root)
+    assert len(commands.args) == 1
+    seq = commands.args[0]
+    assert isinstance(seq, KSequence)
+    return seq
+
+
+def command_is_new_wasm_instance(root: KInner) -> bool:
+    seq = commands_cell_contents(root)
+    if not seq.items:
+        return False
+    first = seq.items[0]
+    if not isinstance(first, KApply):
+        return False
+    return first.label.name == 'newWasmInstance'
+
+
+def set_commands_cell_contents(root: KInner, contents: KSequence) -> KInner:
+    return set_ksequence_cell_contents(root, COMMANDS_CELL_NAME, contents)
+
+
+def set_k_cell_contents(root: KInner, contents: KSequence) -> KInner:
+    return set_ksequence_cell_contents(root, '<k>', contents)
+
+
+def get_wasm_cell(root: KInner) -> KApply:
+    return find_single_named_node(root, WASM_CELL_NAME)
+
+
+def replace_wasm_cell(root: KInner, replacement: KInner) -> KInner:
+    return replace_with_path(root, WASM_CELL_PATH, replacement=replacement)
+
+
+def get_contract_mod_idx_cell(root: KInner) -> KApply:
+    return find_single_named_node(root, CONTRACT_MOD_IDX_CELL_NAME)
+
+
+def replace_contract_mod_idx_cell(root: KInner, replacement: KInner) -> KInner:
+    return replace_with_path(root, CONTRACT_MOD_IDX_CELL_PATH, replacement=replacement)
+
+
+def set_call_stack_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<callStack>', replacement)
+
+
+def set_interim_states_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<interimStates>', replacement)
+
+
+def set_accounts_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<accounts>', replacement)
+
+
+def set_logging_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<logging>', replacement)
+
+
+def set_generated_counter_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<generatedCounter>', replacement)
+
+
+def set_call_args_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<callArgs>', replacement)
+
+
+def set_big_int_heap_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<bigIntHeap>', replacement)
+
+
+def set_buffer_heap_cell_content(root: KInner, replacement: KInner) -> KInner:
+    return set_single_argument_kapply_contents(root, '<bufferHeap>', replacement)
diff --git a/kmxwasm/src/kmxwasm/ast/generic.py b/kmxwasm/src/kmxwasm/ast/generic.py
new file mode 100644
index 00000000..c658a30f
--- /dev/null
+++ b/kmxwasm/src/kmxwasm/ast/generic.py
@@ -0,0 +1,50 @@
+from pyk.kast.inner import KApply, KInner, KSequence, bottom_up
+
+
+def set_single_argument_kapply_contents(root: KInner, name: str, contents: KInner) -> KInner:
+    already_replaced = False
+
+    def replace_contents(node: KInner) -> KInner:
+        if not isinstance(node, KApply):
+            return node
+        if node.label.name != name:
+            return node
+
+        nonlocal already_replaced
+        assert not already_replaced
+        already_replaced = True
+
+        assert len(node.args) == 1
+        return node.let(args=[contents])
+
+    return bottom_up(replace_contents, root)
+
+
+def set_ksequence_cell_contents(root: KInner, name: str, contents: KSequence) -> KInner:
+    return set_single_argument_kapply_contents(root, name, contents)
+
+
+def replace_with_path(root: KInner, path: list[str], replacement: KInner) -> KInner:
+    assert path
+    assert isinstance(root, KApply)
+    assert root.args
+    had_match = False
+    new_args = []
+    for arg in root.args:
+        if not isinstance(arg, KApply):
+            new_args.append(arg)
+            continue
+        if not arg.label.name == path[0]:
+            new_args.append(arg)
+            continue
+        if had_match:
+            raise ValueError(f'Path component found twice: {path[0]!r}')
+        assert not had_match
+        had_match = True
+        if len(path) > 1:
+            new_args.append(replace_with_path(arg, path[1:], replacement))
+        else:
+            new_args.append(replacement)
+    if not had_match:
+        raise ValueError(f'Path component not found: {path[0]!r}')
+    return root.let(args=new_args)
diff --git a/kmxwasm/src/kmxwasm/ast/wasm.py b/kmxwasm/src/kmxwasm/ast/wasm.py
index ec868eb6..75f2d564 100644
--- a/kmxwasm/src/kmxwasm/ast/wasm.py
+++ b/kmxwasm/src/kmxwasm/ast/wasm.py
@@ -1,8 +1,9 @@
 from typing import Iterable
 
-from pyk.kast.inner import KApply, KInner
+from pyk.kast.inner import KApply, KInner, KSequence
 
 from .collections import cell_map, simple_list
+from .generic import set_ksequence_cell_contents
 
 # TODO: Move these to the wasm-semantics repository
 
@@ -33,3 +34,7 @@ def valStack(items: Iterable[KInner]) -> KInner:  # noqa: N802
 
 def optionalInt_empty() -> KInner:  # noqa: N802
     return KApply('.Int')
+
+
+def set_instrs_cell_contents(root: KInner, contents: KSequence) -> KInner:
+    return set_ksequence_cell_contents(root, '<instrs>', contents)
diff --git a/kmxwasm/src/kmxwasm/build.py b/kmxwasm/src/kmxwasm/build.py
index 0f6cf1e9..63a7bcc1 100644
--- a/kmxwasm/src/kmxwasm/build.py
+++ b/kmxwasm/src/kmxwasm/build.py
@@ -1,3 +1,4 @@
+import time
 from pathlib import Path
 
 from pyk.kbuild.kbuild import KBuild
@@ -5,9 +6,14 @@
 
 from .tools import Tools
 
+HASKELL = 'haskell'
+LLVM = 'llvm'
 
-def kbuild_semantics(output_dir: Path, config_file: Path) -> Tools:
+
+def kbuild_semantics(output_dir: Path, config_file: Path, target: str) -> Tools:
     kbuild = KBuild(output_dir)
     package = Package.create(config_file)
-    kbuild.kompile(package, 'haskell')
-    return Tools(kbuild.definition_dir(package, 'haskell'))
+    start_time = time.time()
+    kbuild.kompile(package, target)
+    print('Kompiling', target, ':', time.time() - start_time, 'sec')
+    return Tools(kbuild.definition_dir(package, target))
diff --git a/kmxwasm/src/kmxwasm/json.py b/kmxwasm/src/kmxwasm/json.py
index 9ab828f4..44ced677 100644
--- a/kmxwasm/src/kmxwasm/json.py
+++ b/kmxwasm/src/kmxwasm/json.py
@@ -2,6 +2,7 @@
 from pathlib import Path
 from typing import Any, Mapping
 
+from pyk.kast import kast_term
 from pyk.kast.inner import KInner
 from pyk.kast.outer import KClaim
 from pyk.kcfg import KCFG
@@ -30,7 +31,7 @@ def load_json_kcfg(input_file: Path) -> KCFG:
 
 def load_json_kclaim(input_file: Path) -> KClaim:
     value = load_json_dict(input_file)
-    return KClaim.from_dict(value)
+    return kast_term(value, KClaim)
 
 
 def write_json(term_dict: dict[str, Any], output_file: Path) -> None:
diff --git a/kmxwasm/src/kmxwasm/proofs.py b/kmxwasm/src/kmxwasm/proofs.py
index 20dc2e46..d2e7f2d3 100644
--- a/kmxwasm/src/kmxwasm/proofs.py
+++ b/kmxwasm/src/kmxwasm/proofs.py
@@ -301,7 +301,7 @@ def my_step(explorer: LazyExplorer, kcfg: KCFG, node_id: int) -> List[int]:
 
     print(f'Executing {node.id}!', flush=True)
     try:
-        (depth, cterm, next_cterms, next_node_logs) = explorer.get().cterm_execute(
+        (_is_vacuous, depth, cterm, next_cterms, next_node_logs) = explorer.get().cterm_execute(
             node.cterm, depth=1, module_name=GENERATED_MODULE_NAME
         )
     except BaseException:
diff --git a/kmxwasm/src/kmxwasm/property.py b/kmxwasm/src/kmxwasm/property.py
index 169bef8d..f9301c46 100644
--- a/kmxwasm/src/kmxwasm/property.py
+++ b/kmxwasm/src/kmxwasm/property.py
@@ -9,11 +9,12 @@
 from pyk.kcfg.show import KCFGShow
 from pyk.kore.rpc import KoreClientError
 
-from .build import kbuild_semantics
+from .build import HASKELL, LLVM, kbuild_semantics
 from .json import load_json_kcfg, load_json_kclaim, write_kcfg_json
 from .paths import KBUILD_DIR, KBUILD_ML_PATH, ROOT
 from .printers import print_node
 from .running import RunException, Stuck, Success, run_claim, split_edge
+from .wasm_krun_initializer import WasmKrunInitializer
 
 # TODO: Make this work outside of github projects.
 DEBUG_KCFG = ROOT / '.property' / 'kcfg.json'
@@ -50,7 +51,10 @@ class RunClaim(Action):
     depth: int
 
     def run(self) -> None:
-        with kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH) as tools:
+        with (
+            kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH, target=HASKELL) as tools,
+            kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH, target=LLVM) as llvm_tools,
+        ):
             if self.is_k:
                 claims = tools.kprove.get_claims(self.claim_path)
                 if len(claims) != 1:
@@ -65,7 +69,14 @@ def run(self) -> None:
                 kcfg = load_json_kcfg(DEBUG_KCFG)
                 for node_id in self.remove:
                     kcfg.remove_node(node_id)
-            result = run_claim(tools, claim, kcfg, run_id=self.run_node_id, depth=self.depth)
+            result = run_claim(
+                tools,
+                WasmKrunInitializer(llvm_tools),
+                claim=claim,
+                restart_kcfg=kcfg,
+                run_id=self.run_node_id,
+                depth=self.depth,
+            )
             write_kcfg_json(result.kcfg, DEBUG_KCFG)
 
             if isinstance(result, Stuck):
@@ -121,7 +132,7 @@ class BisectAfter(Action):
     node_id: int
 
     def run(self) -> None:
-        with kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH) as tools:
+        with kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH, target=HASKELL) as tools:
             kcfg = load_json_kcfg(DEBUG_KCFG)
 
             result = split_edge(tools, kcfg, start_node_id=self.node_id)
@@ -158,7 +169,7 @@ class ShowNode(Action):
     node_id: int
 
     def run(self) -> None:
-        with kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH) as tools:
+        with kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH, target=HASKELL) as tools:
             kcfg = load_json_kcfg(DEBUG_KCFG)
             print('Printing: ', self.node_id)
             node = kcfg.get_node(self.node_id)
@@ -171,7 +182,7 @@ def run(self) -> None:
 @dataclass(frozen=True)
 class Tree(Action):
     def run(self) -> None:
-        with kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH) as tools:
+        with kbuild_semantics(output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH, target=HASKELL) as tools:
             kcfg = load_json_kcfg(DEBUG_KCFG)
             show = KCFGShow(tools.printer)
             for line in show.pretty(kcfg):
diff --git a/kmxwasm/src/kmxwasm/running.py b/kmxwasm/src/kmxwasm/running.py
index 4c71c6dd..725533d8 100644
--- a/kmxwasm/src/kmxwasm/running.py
+++ b/kmxwasm/src/kmxwasm/running.py
@@ -3,10 +3,14 @@
 
 from pyk.kast.outer import KClaim
 from pyk.kcfg import KCFG
+from pyk.kcfg.exploration import KCFGExploration
 from pyk.kcfg.kcfg import NodeIdLike
 from pyk.kore.rpc import LogEntry
 
+from .ast.elrond import command_is_new_wasm_instance
+from .printers import print_node
 from .tools import Tools
+from .wasm_krun_initializer import WasmKrunInitializer
 
 
 @dataclass(frozen=True)
@@ -31,7 +35,14 @@ class RunException(RunClaimResult):
     last_processed_node: NodeIdLike
 
 
-def run_claim(tools: Tools, claim: KClaim, restart_kcfg: KCFG | None, run_id: int | None, depth: int) -> RunClaimResult:
+def run_claim(
+    tools: Tools,
+    wasm_initializer: WasmKrunInitializer,
+    claim: KClaim,
+    restart_kcfg: KCFG | None,
+    run_id: int | None,
+    depth: int,
+) -> RunClaimResult:
     last_processed_node: NodeIdLike = -1
     init_node_id: NodeIdLike = -1
     target_node_id: NodeIdLike = -1
@@ -56,6 +67,8 @@ def run_claim(tools: Tools, claim: KClaim, restart_kcfg: KCFG | None, run_id: in
     else:
         (kcfg, init_node_id, target_node_id) = KCFG.from_claim(tools.printer.definition, claim)
 
+    kcfg_exploration = KCFGExploration(kcfg)
+
     try:
         processed: set[NodeIdLike] = {target_node_id}
         non_final: set[NodeIdLike] = {target_node_id}
@@ -82,7 +95,17 @@ def run_claim(tools: Tools, claim: KClaim, restart_kcfg: KCFG | None, run_id: in
 
                 logs: dict[int, tuple[LogEntry, ...]] = {}
                 try:
-                    tools.explorer.extend(kcfg=kcfg, node=node, logs=logs, execute_depth=depth)
+                    if command_is_new_wasm_instance(node.cterm.config):
+                        print('is new wasm')
+                        wasm_initializer.initialize(kcfg=kcfg, start_node=node)
+                    else:
+                        tools.explorer.extend(
+                            kcfg_exploration=kcfg_exploration,
+                            node=node,
+                            logs=logs,
+                            execute_depth=depth,
+                            cut_point_rules=['ELROND-CONFIG.newWasmInstance'],
+                        )
                     for node in kcfg.leaves:
                         if node.id not in non_final:
                             non_final.add(node.id)
@@ -128,6 +151,8 @@ def split_edge(tools: Tools, restart_kcfg: KCFG, start_node_id: int) -> RunClaim
             target_node_id = roots[0].id
     final_node = kcfg.node(target_node_id)
 
+    kcfg_exploration = KCFGExploration(kcfg)
+
     try:
         # preecompute the explorer to make time measurements more reliable.
         assert tools.explorer
@@ -153,7 +178,7 @@ def split_edge(tools: Tools, restart_kcfg: KCFG, start_node_id: int) -> RunClaim
 
         logs: dict[int, tuple[LogEntry, ...]] = {}
 
-        tools.explorer.extend(kcfg=kcfg, node=start, logs=logs, execute_depth=half_depth)
+        tools.explorer.extend(kcfg_exploration=kcfg_exploration, node=start, logs=logs, execute_depth=half_depth)
         middle_node: KCFG.Node | None = None
         for node in kcfg.leaves:
             if node.id in to_ignore:
@@ -168,7 +193,9 @@ def split_edge(tools: Tools, restart_kcfg: KCFG, start_node_id: int) -> RunClaim
         middle_time = time.time()
         print(f'{start.id} -> {middle_node.id}: {middle_time-start_time} sec')
 
-        tools.explorer.extend(kcfg=kcfg, node=middle_node, logs=logs, execute_depth=total_depth - half_depth)
+        tools.explorer.extend(
+            kcfg_exploration=kcfg_exploration, node=middle_node, logs=logs, execute_depth=total_depth - half_depth
+        )
         result_node: KCFG.Node | None = None
         for node in kcfg.leaves:
             if node.id in to_ignore:
@@ -179,6 +206,15 @@ def split_edge(tools: Tools, restart_kcfg: KCFG, start_node_id: int) -> RunClaim
         assert result_node
 
         csubst = tools.explorer.cterm_implies(result_node.cterm, destination.cterm)
+        if not csubst:
+            print('*' * 30, 'Antecedent', '*' * 30)
+            print_node(tools, result_node)
+            print('*' * 30, 'Consequent', '*' * 30)
+            print_node(tools, destination)
+            (success, reason) = tools.explorer.implication_failure_reason(
+                antecedent=result_node.cterm, consequent=destination.cterm
+            )
+            raise ValueError(f'Implies failure, {[success, reason]}')
         assert csubst is not None
 
         replaced_edge = kcfg.edge(source_id=middle_node.id, target_id=result_node.id)
diff --git a/kmxwasm/src/kmxwasm/specs.py b/kmxwasm/src/kmxwasm/specs.py
index ea26feeb..f922e77e 100644
--- a/kmxwasm/src/kmxwasm/specs.py
+++ b/kmxwasm/src/kmxwasm/specs.py
@@ -39,7 +39,12 @@ def __has_dependencies(spec_dependencies: List[str], processed_functions: List[s
     def __prove(spec_path: Path, kprove: KProve) -> None:
         print(f'Proving {spec_path}', flush=True)
         final_state = kprove.prove(spec_path)
-        if not is_top(final_state):
+        if not len(final_state) == 1:
+            raise ValueError(f'Failed to prove {spec_path}.')
+        final_cterm = final_state[0]
+        if final_cterm.constraints:
+            raise ValueError(f'Failed to prove {spec_path}.')
+        if not is_top(final_cterm.config):
             raise ValueError(f'Failed to prove {spec_path}.')
         print('Proving done', flush=True)
 
diff --git a/kmxwasm/src/kmxwasm/tools.py b/kmxwasm/src/kmxwasm/tools.py
index 7ef7e528..784b39a4 100644
--- a/kmxwasm/src/kmxwasm/tools.py
+++ b/kmxwasm/src/kmxwasm/tools.py
@@ -1,11 +1,17 @@
+import json
 from pathlib import Path
+from tempfile import NamedTemporaryFile
 from typing import Any, Optional
 
+from pyk.kast.inner import KInner
+from pyk.kast.kast import kast_term
 from pyk.kast.pretty import SymbolTable
 from pyk.kcfg.explore import KCFGExplore
 from pyk.kore.rpc import KoreClient, KoreServer
 from pyk.ktool.kprint import KPrint
 from pyk.ktool.kprove import KProve
+from pyk.ktool.krun import KRunOutput, _krun
+from pyk.prelude.k import GENERATED_TOP_CELL
 
 
 class Tools:
@@ -55,6 +61,21 @@ def explorer(self) -> KCFGExplore:
             self.__explorer = KCFGExplore(self.printer, self.__kore_client)
         return self.__explorer
 
+    def krun(self, cfg: KInner) -> KInner:
+        with NamedTemporaryFile('w') as ntf:
+            pattern = self.printer.kast_to_kore(cfg, sort=GENERATED_TOP_CELL)
+            ntf.write(pattern.text)
+            ntf.flush()
+            result = _krun(
+                input_file=Path(ntf.name),
+                definition_dir=self.__definition_dir,
+                output=KRunOutput.JSON,
+                term=True,
+                parser='cat',
+            )
+            value = json.loads(result.stdout)
+            return kast_term(value, KInner)  # type: ignore # https://github.com/python/mypy/issues/4717
+
 
 def my_patch_symbol_table(symbol_table: SymbolTable) -> None:
     symbol_table['_|->_'] = lambda c1, c2: f'({c1} |-> {c2})'
@@ -90,11 +111,14 @@ def my_patch_symbol_table(symbol_table: SymbolTable) -> None:
 
     symbol_table['~Int_'] = lambda c1: f'~Int ({c1})'
     symbol_table['_modInt_'] = lambda c1, c2: f'({c1}) modInt ({c2})'
-    symbol_table['_modIntTotal_'] = lambda c1, c2: f'({c1}) modIntTotal ({c2})'
+    symbol_table['modIntTotal'] = lambda c1, c2: f'({c1}) modIntTotal ({c2})'
+    symbol_table['_divInt_'] = lambda c1, c2: f'({c1}) divInt ({c2})'
+    symbol_table['divIntTotal'] = lambda c1, c2: f'({c1}) divIntTotal ({c2})'
     symbol_table['_*Int_'] = lambda c1, c2: f'({c1}) *Int ({c2})'
     symbol_table['_/Int_'] = lambda c1, c2: f'({c1}) /Int ({c2})'
-    symbol_table['_/IntTotal_'] = lambda c1, c2: f'({c1}) /Int ({c2})'
+    symbol_table['_/IntTotal_'] = lambda c1, c2: f'({c1}) /IntTotal ({c2})'
     symbol_table['_%Int_'] = lambda c1, c2: f'({c1}) %Int ({c2})'
+    symbol_table['_%IntTotal_'] = lambda c1, c2: f'({c1}) %IntTotal ({c2})'
     symbol_table['_^Int_'] = lambda c1, c2: f'({c1}) ^Int ({c2})'
     symbol_table['_^%Int_'] = lambda c1, c2: f'({c1}) ^%Int ({c2})'
     symbol_table['_+Int_'] = lambda c1, c2: f'({c1}) +Int ({c2})'
diff --git a/kmxwasm/src/kmxwasm/wasm_krun_initializer.py b/kmxwasm/src/kmxwasm/wasm_krun_initializer.py
new file mode 100644
index 00000000..0176abe4
--- /dev/null
+++ b/kmxwasm/src/kmxwasm/wasm_krun_initializer.py
@@ -0,0 +1,71 @@
+from pyk.cterm import CTerm
+from pyk.kast.inner import KInner, KSequence
+from pyk.kcfg import KCFG
+from pyk.prelude.collections import list_of, map_empty
+from pyk.prelude.utils import token
+
+from .ast.elrond import (
+    accountCellMap,
+    commands_cell_contents,
+    get_contract_mod_idx_cell,
+    get_wasm_cell,
+    listBytes,
+    mapIntToBytes,
+    replace_contract_mod_idx_cell,
+    replace_wasm_cell,
+    set_accounts_cell_content,
+    set_big_int_heap_cell_content,
+    set_buffer_heap_cell_content,
+    set_call_args_cell_content,
+    set_call_stack_cell_content,
+    set_commands_cell_contents,
+    set_generated_counter_cell_content,
+    set_interim_states_cell_content,
+    set_k_cell_contents,
+    set_logging_cell_content,
+)
+from .ast.wasm import set_instrs_cell_contents
+from .tools import Tools
+
+
+class WasmKrunInitializer:
+    def __init__(self, tools: Tools):
+        self.__tools = tools
+        self.__first_wasm_cell: KInner | None = None
+
+    def initialize(self, kcfg: KCFG, start_node: KCFG.Node) -> None:
+        start_cell = start_node.cterm.config
+        commands_contents = commands_cell_contents(start_cell)
+        assert len(commands_contents) > 0
+        first = commands_contents.items[0]
+
+        krun_cell = set_call_stack_cell_content(start_cell, list_of([]))
+        if not self.__first_wasm_cell:
+            # This must run after set_call_stack_cell_content because the call
+            # stack also contains <wasm> entries, which makes get_wasm_cell crash.
+            self.__first_wasm_cell = get_wasm_cell(krun_cell)
+        krun_cell = set_k_cell_contents(krun_cell, KSequence([]))
+        krun_cell = set_commands_cell_contents(krun_cell, KSequence([first]))
+        krun_cell = set_instrs_cell_contents(krun_cell, KSequence([]))
+        krun_cell = set_interim_states_cell_content(krun_cell, list_of([]))
+        krun_cell = set_accounts_cell_content(krun_cell, accountCellMap([]))
+        krun_cell = set_logging_cell_content(krun_cell, token(''))
+        krun_cell = set_generated_counter_cell_content(krun_cell, token(0))
+        krun_cell = set_call_args_cell_content(krun_cell, listBytes([]))
+        krun_cell = set_big_int_heap_cell_content(krun_cell, map_empty())
+        krun_cell = set_buffer_heap_cell_content(krun_cell, mapIntToBytes({}))
+        krun_cell = replace_wasm_cell(krun_cell, self.__first_wasm_cell)
+
+        # TODO: Figure out if it's possible to cache the initialization result.
+        print('*' * 30, 'Initializing WASM.')
+        krun_result = self.__tools.krun(krun_cell)
+
+        wasm_cell = get_wasm_cell(krun_result)
+        final_cell = replace_wasm_cell(start_cell, wasm_cell)
+        current_module = get_contract_mod_idx_cell(krun_result)
+        final_cell = replace_contract_mod_idx_cell(final_cell, current_module)
+        final_cell = set_commands_cell_contents(final_cell, KSequence(commands_contents.items[1:]))
+
+        final_cterm = CTerm(final_cell, start_node.cterm.constraints)
+        final_node = kcfg.create_node(final_cterm)
+        kcfg.create_edge(source_id=start_node.id, target_id=final_node.id, depth=1)
diff --git a/kmxwasm/src/tests/integration/test_claims.py b/kmxwasm/src/tests/integration/test_claims.py
index 94e1b58e..91b54dd4 100644
--- a/kmxwasm/src/tests/integration/test_claims.py
+++ b/kmxwasm/src/tests/integration/test_claims.py
@@ -20,10 +20,11 @@
     tabInstCellMap,
     valStack,
 )
-from kmxwasm.build import kbuild_semantics
+from kmxwasm.build import HASKELL, kbuild_semantics
 from kmxwasm.paths import KBUILD_ML_PATH
 from kmxwasm.running import Success, run_claim
 from kmxwasm.tools import Tools
+from kmxwasm.wasm_krun_initializer import WasmKrunInitializer
 
 sys.setrecursionlimit(1500000000)
 
@@ -156,7 +157,7 @@ def full_configuration(
 @pytest.fixture(scope='module')
 def tools(tmp_path_factory: TempPathFactory) -> Tools:
     build_path = tmp_path_factory.mktemp('kbuild')
-    tools = kbuild_semantics(output_dir=build_path, config_file=KBUILD_ML_PATH)
+    tools = kbuild_semantics(output_dir=build_path, config_file=KBUILD_ML_PATH, target=HASKELL)
     return tools
 
 
@@ -219,5 +220,5 @@ class TestSimpleProofs:
         ids=[test_id for test_id, *_ in SIMPLE_PROOFS_DATA],
     )
     def test_run_claim(self, tools: Tools, test_id: str, claim: KClaim, success: bool) -> None:
-        result = run_claim(tools, claim, restart_kcfg=None, run_id=None, depth=1000)
+        result = run_claim(tools, WasmKrunInitializer(tools), claim, restart_kcfg=None, run_id=None, depth=1000)
         assert isinstance(result, Success) == success