Z3 Substitution of Bound Variables Failing Due to Sort Mismatch, but Correct Sort Used

[baierd]

CPAchecker found some regressions for Z3 in (more or less) current main here. When trying to substitute the bound variables we get a sort mismatch, as Z3 expects argument number 2 to be a function (declare-fun bvadd ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32)), which is incorrect, as we know argument #2 to be of sort (Array (_ BitVec 32) (_ BitVec 32)).

I opened a issue in the Z3 repo here.

[baierd]

Closed with merge of PR 535.