The translation of Act to Expr is not faithful to the Solidity storage layout for values shorted than a word. The current translation naively puts every storage value in 256bit word slots. As a result, equivalence for the following fails:

constructor of A
interface constructor()

iff

  CALLVALUE == 0

creates

  uint128 x := 11
  uint128 y := 42

contract A {
    uint128 x;
    uint128 y;
    
    constructor() {
        x = 11;
        y = 42;
    }
}

Correct encoding of the layout will also fix #175.