GlobalDDE fails remove dead functions and axioms involving bitvector functions

[delcypher]

This issue was report by @akashlal

Here's an example program that triggers the bug

function {:bvbuiltin "bvadd"} BVADD32(bv32,bv32) returns (bv32);

// GlobalDDE fails to remove this dead function and axiom because
// it conservatively assumes that the used BVADD32 is related to
// ADD_ONE and because BVADD32 is used that the axiom might constrain
// BVADD32's behaviour in someway
function ADD_ONE(bv32) returns (bv32);
axiom (forall x:bv32 :: ADD_ONE(x) == BVADD32(x, 1bv32));

procedure main() {
    var x:bv32;
    var y:bv32;

    x := BVADD32(x, y);
    assert x == BVADD32(x, y);
}

[delcypher]

Fixed by 24cab969a1ff90e9eaebc591e3a6978ee5066b78