Simplification is not equivalent, but it should be

[msooseth]

      let e = PEq (BufLength (AbstractBuf "esc_buf_CugleWOwEWXP")) (Lit 0)
      let simp = Expr.simplifyProp e
      let simpExpected = PEq (AbstractBuf "esc_buf_CugleWOwEWXP") (ConcreteBuf "")
      assertEqualM "buflen-to-empty" simp simpExpected
      ret <- checkEquivPropAndLHS e simpExpected
      assertBoolM "Must be equivalent" ret

Somehow we get a CEX, even though this simplification is good. I'll look into this. Triggered at: https://github.com/ethereum/hevm/actions/runs/13362022051/job/37313197906?pr=663 in PR #663 by @elopez

[msooseth]

Oh wow, so this somehow is SAT:

   1   │ ;(PNeg
   2   │ ;  (PAnd
   3   │ ;    (PImpl
   4   │ ;      (PEq
   5   │ ;        (BufLength
   6   │ ;          (AbstractBuf "mybuf")
   7   │ ;        )
   8   │ ;        0
   9   │ ;      )
  10   │ ;      (PEq
  11   │ ;        (AbstractBuf "mybuf")
  12   │ ;        (ConcreteBuf "")
  13   │ ;      )
  14   │ ;    )
  15   │ ;    (PImpl
  16   │ ;      (PEq
  17   │ ;        (AbstractBuf "mybuf")
  18   │ ;        (ConcreteBuf "")
  19   │ ;      )
  20   │ ;      (PEq
  21   │ ;        (BufLength
  22   │ ;          (AbstractBuf "mybuf")
  23   │ ;        )
  24   │ ;        0
  25   │ ;      )
  26   │ ;    )
  27   │ ;  )
  28   │ ;)

which sounds wrong. buflength=0 should imply and empty buf, and an empty buf should emply buflength=0.