diff --git a/src/kontrol/utils.py b/src/kontrol/utils.py
index 2cdc91f85..50e312472 100644
--- a/src/kontrol/utils.py
+++ b/src/kontrol/utils.py
@@ -306,6 +306,7 @@ def replace_k_words(text: str) -> str:
         '#Equals': '==',
         'NUMBER_CELL': 'block.number',
         'TIMESTAMP_CELL': 'block.timestamp',
+        'MIXHASH_CELL': 'block.prevrandao',
         ':Int': '',
         ':Bytes': '',
     }
diff --git a/src/tests/integration/test-data/end-to-end-prove-all b/src/tests/integration/test-data/end-to-end-prove-all
index 68b08a2c4..5f71105df 100644
--- a/src/tests/integration/test-data/end-to-end-prove-all
+++ b/src/tests/integration/test-data/end-to-end-prove-all
@@ -56,4 +56,5 @@ UnitTest.test_assertNotEq(bytes32,bytes32)
 UnitTest.test_assertNotEq(int256,int256)
 UnitTest.test_assertTrue_err()
 UnitTest.test_assertTrue(bool)
-UnitTest.test_checkInitialBalance(uint256)
\ No newline at end of file
+UnitTest.test_checkInitialBalance(uint256)
+UnitTest.test_prevrandao_nonnegative()
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/UnitTest.test_checkInitialBalance(uint256).expected b/src/tests/integration/test-data/show/UnitTest.test_checkInitialBalance(uint256).expected
index ac1f86a43..291e26644 100644
--- a/src/tests/integration/test-data/show/UnitTest.test_checkInitialBalance(uint256).expected
+++ b/src/tests/integration/test-data/show/UnitTest.test_checkInitialBalance(uint256).expected
@@ -4,13 +4,13 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/Unit.t.sol:6:458
+│   src: test/Unit.t.sol:6:462
 │   method: test%UnitTest.test_checkInitialBalance(uint256)
 │
 │  (880 steps)
 ├─ 3
 │   k: #consoleLog 3054400204 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0 ...
-│   pc: 16676
+│   pc: 16687
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │   src: lib/forge-std/src/console.sol:11:22
@@ -19,7 +19,7 @@
 │  (1 step)
 ├─ 4
 │   k: #refund 0 ~> 1 ~> #push ~> #setLocalMem 0 0 b"" ~> #pc [ STATICCALL ] ~> #execut ...
-│   pc: 16676
+│   pc: 16687
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │   src: lib/forge-std/src/console.sol:11:22
@@ -28,7 +28,7 @@
 │  (646 steps)
 ├─ 5
 │   k: #consoleLog 3054400204 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0 ...
-│   pc: 16676
+│   pc: 16687
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │   src: lib/forge-std/src/console.sol:11:22
@@ -37,7 +37,7 @@
 │  (1 step)
 ├─ 6
 │   k: #refund 0 ~> 1 ~> #push ~> #setLocalMem 0 0 b"" ~> #pc [ STATICCALL ] ~> #execut ...
-│   pc: 16676
+│   pc: 16687
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │   src: lib/forge-std/src/console.sol:11:22
@@ -46,7 +46,7 @@
 │  (205 steps)
 ├─ 7 (terminal)
 │   k: #halt ~> CONTINUATION:K
-│   pc: 1038
+│   pc: 1049
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │   src: test/Unit.t.sol:135:139
@@ -115,7 +115,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( #address ( FoundryConsole ) : ( 192 : ( 2095 : ( 192 : ( 2280 : ( maxUInt96 : ( 128 : ( 10324 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) )
+                     ( .WordStack => ( #address ( FoundryConsole ) : ( 192 : ( 2106 : ( 192 : ( 2291 : ( maxUInt96 : ( 128 : ( 10335 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
@@ -341,7 +341,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( #address ( FoundryConsole ) : ( 192 : ( 2095 : ( 192 : ( 2280 : ( maxUInt96 : ( 128 : ( 10324 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
+                     ( #address ( FoundryConsole ) : ( 192 : ( 2106 : ( 192 : ( 2291 : ( maxUInt96 : ( 128 : ( 10335 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
@@ -567,7 +567,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( #address ( FoundryConsole ) : ( ( 192 => 420 ) : ( 2095 : ( ( 192 => 420 ) : ( 2280 : ( ( maxUInt96 => KV0_amount:Int ) : ( ( 128 => 356 ) : ( ( 10324 => 10372 ) : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
+                     ( #address ( FoundryConsole ) : ( ( 192 => 420 ) : ( 2106 : ( ( 192 => 420 ) : ( 2291 : ( ( maxUInt96 => KV0_amount:Int ) : ( ( 128 => 356 ) : ( ( 10335 => 10383 ) : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02H\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , KV0_amount:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
@@ -793,7 +793,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( #address ( FoundryConsole ) : ( 420 : ( 2095 : ( 420 : ( 2280 : ( KV0_amount:Int : ( 356 : ( 10372 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
+                     ( #address ( FoundryConsole ) : ( 420 : ( 2106 : ( 420 : ( 2291 : ( KV0_amount:Int : ( 356 : ( 10383 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02H\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , KV0_amount:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
@@ -1021,7 +1021,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( ( #address ( FoundryConsole ) => 3050190935 ) : ( ( 420 : ( 2095 : ( 420 : ( 2280 : ( KV0_amount:Int : ( 356 : ( 10372 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) => .WordStack ) )
+                     ( ( #address ( FoundryConsole ) => 3050190935 ) : ( ( 420 : ( 2106 : ( 420 : ( 2291 : ( KV0_amount:Int : ( 356 : ( 10383 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) => .WordStack ) )
                    </wordStack>
                    <localMem>
                      b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02H\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , KV0_amount:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
diff --git a/src/tests/integration/test-data/show/UnitTestCounterexampleTest.expected b/src/tests/integration/test-data/show/UnitTestCounterexampleTest.expected
index 7a45f5aa8..0c5ae4fd8 100644
--- a/src/tests/integration/test-data/show/UnitTestCounterexampleTest.expected
+++ b/src/tests/integration/test-data/show/UnitTestCounterexampleTest.expected
@@ -400,7 +400,7 @@ contract UnitTest is Test {
         val1[2] = 0; val2[2] = 0;
         string memory err = "throw test";
         string memory err_output = "throw test: [-1, 2, 0] != [1, -2, 0]";
-        vm.expectRevert(bytes(err_output));        
+        vm.expectRevert(bytes(err_output));
         assertEq(val1, val2, err);
     }
 
@@ -425,9 +425,9 @@ contract UnitTest is Test {
         val1[2] = 2; val2[2] = 12;
         val1[3] = 3; val2[3] = 13;
         val1[4] = 4; val2[4] = 14;
-        string memory err = "throw test";  
+        string memory err = "throw test";
         string memory err_output = "throw test: [0, 1, 2, 3, 4] != [10, 11, 12, 13, 14]";
-        vm.expectRevert(bytes(err_output));      
+        vm.expectRevert(bytes(err_output));
         assertEq(val1, val2, err);
     }
 
@@ -444,6 +444,10 @@ contract UnitTest is Test {
         assert(value != 10);
     }
 
+    function test_prevrandao_nonnegative() public view {
+       assert(block.prevrandao >= 0);
+    }
+
     /****************************
     * Internal helper functions *
     *****************************/
diff --git a/src/tests/integration/test-data/test/Unit.t.sol b/src/tests/integration/test-data/test/Unit.t.sol
index c065dc40f..d22cf5abb 100644
--- a/src/tests/integration/test-data/test/Unit.t.sol
+++ b/src/tests/integration/test-data/test/Unit.t.sol
@@ -400,7 +400,7 @@ contract UnitTest is Test {
         val1[2] = 0; val2[2] = 0;
         string memory err = "throw test";
         string memory err_output = "throw test: [-1, 2, 0] != [1, -2, 0]";
-        vm.expectRevert(bytes(err_output));        
+        vm.expectRevert(bytes(err_output));
         assertEq(val1, val2, err);
     }
 
@@ -425,9 +425,9 @@ contract UnitTest is Test {
         val1[2] = 2; val2[2] = 12;
         val1[3] = 3; val2[3] = 13;
         val1[4] = 4; val2[4] = 14;
-        string memory err = "throw test";  
+        string memory err = "throw test";
         string memory err_output = "throw test: [0, 1, 2, 3, 4] != [10, 11, 12, 13, 14]";
-        vm.expectRevert(bytes(err_output));      
+        vm.expectRevert(bytes(err_output));
         assertEq(val1, val2, err);
     }
 
@@ -444,6 +444,10 @@ contract UnitTest is Test {
         assert(value != 10);
     }
 
+    function test_prevrandao_nonnegative() public view {
+       assert(block.prevrandao >= 0);
+    }
+
     /****************************
     * Internal helper functions *
     *****************************/