diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 42836d815c..41621facb5 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.464"
+version = "1.0.465"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index e84c42b0f0..1f16de7190 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.464'
+VERSION: Final = '1.0.465'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
index 5f9afc696f..8105513129 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -749,10 +749,23 @@ These are just used by the other operators for shuffling local execution state a
 ```k
     syntax InternalOp ::= "#newAccount" Int
                         | "#newExistingAccount" Int
-                        | "#newFreshAccount" Int
  // --------------------------------------------
     rule <k> #newAccount ACCT => #newExistingAccount ACCT ... </k> <account> <acctID> ACCT </acctID> ... </account>
-    rule <k> #newAccount ACCT => #newFreshAccount ACCT    ... </k> [owise]
+    rule <k> #newAccount ACCT => .    ... </k>
+             <accounts>
+               ( .Bag
+                  =>
+                 <account>
+                    <acctID> ACCT </acctID>
+                    <balance>     0                  </balance>
+                    <code>        .Bytes:AccountCode </code>
+                    <storage>     .Map               </storage>
+                    <origStorage> .Map               </origStorage>
+                    <nonce>       0                  </nonce>
+                 </account>
+               )
+               ...
+             </accounts> [owise, preserves-definedness]
 
     rule <k> #newExistingAccount ACCT => #end EVMC_ACCOUNT_ALREADY_EXISTS ... </k>
          <account>
@@ -773,17 +786,6 @@ These are just used by the other operators for shuffling local execution state a
            ...
          </account>
       requires lengthBytes(CODE) ==Int 0
-
-    rule <k> #newFreshAccount ACCT => .K ... </k>
-         <accounts>
-           ( .Bag
-          => <account>
-               <acctID> ACCT </acctID>
-               ...
-             </account>
-           )
-           ...
-         </accounts>
 ```
 
 -   `#transferFunds` moves money from one account into another, creating the destination account if it doesn't exist.
@@ -812,6 +814,7 @@ These are just used by the other operators for shuffling local execution state a
            ...
          </account>
       requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
+      [preserves-definedness]
 
     rule <k> #transferFunds ACCTFROM _ACCTTO VALUE => #end EVMC_BALANCE_UNDERFLOW ... </k>
          <account>
@@ -1365,6 +1368,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
          <accessedStorage> ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... </accessedStorage>
          <schedule> SCHED </schedule>
          requires Ghasaccesslist << SCHED >>
+         [preserves-definedness]
 
     rule <k> #accessStorage ACCT INDEX => .K ... </k>
          <accessedStorage> TS => TS[ACCT <- SetItem(INDEX)] </accessedStorage>
diff --git a/package/version b/package/version
index 42d08cf19a..569c1a0b0c 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.464
+1.0.465
diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster
index 6cc20db2ad..190f2e99ec 100644
--- a/tests/failing-symbolic.haskell-booster
+++ b/tests/failing-symbolic.haskell-booster
@@ -15,6 +15,7 @@ tests/specs/functional/lemmas-no-smt-spec.k
 tests/specs/functional/lemmas-spec.k
 tests/specs/functional/merkle-spec.k
 tests/specs/functional/storageRoot-spec.k
+tests/specs/kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k
 tests/specs/mcd/dstoken-burn-self-fail-rough-spec.k
 tests/specs/mcd/dstoken-transferfrom-fail-rough-spec.k
 tests/specs/mcd/end-cash-pass-rough-spec.k