Adding automated test

CHANGELOG.md

@@ -5,6 +5,11 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## Fixed
+- We now try to simplify expressions fully before trying to cast them to a concrete value
+  This should improve issues when "Unexpected Symbolic Arguments to Opcode" was
+  unnecessarily output
+
 ## [0.54.2] - 2024-12-12
 
 ## Fixed

test/test.hs

@@ -449,6 +449,14 @@ tests = testGroup "hevm"
        expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
        -- putStrLnM $ T.unpack $ formatExpr expr
        assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-wordToAddr" $ do
+       let a = "000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a"
+           s = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)])
+           expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) s
+           simpExpr = Expr.wordToAddr expr
+           simpExpr2 = Expr.concKeccakSimpExpr expr
+       assertEqualM "Expression should simplify to value." simpExpr (Just $ LitAddr 0x5842cf)
+       assertEqualM "Expression should simplify to value." simpExpr2 (Lit 0x5842cf)
     ]
   , testGroup "StorageTests"
     [ test "read-from-sstore" $ assertEqualM ""