Is there any possibility to convert .smt2 formula into equialent one, rewriting it in such way that every (declare-const a (_ BitVec 256)) will be converted into set of (declare-const a0 (_ BitVec 8)). So the maximum BitVec size became 8. But the solution and logic of asserts stay the same?
No such reduction is possible, in general. (i.e., one that would work for arbitrary problems.)
Here's a simple counter-example. Consider the single assertion x > 255 when x is interpreted as a 256-bit variable. This is clearly satisfiable. But when you restrict x to be 8-bits wide, it is not.
Before you ask perhaps we can "scale" the constants accordingly, the answer will stay the same: In general, if you have N 256-bit variables, you have a state space of N^256 bits. If you keep the number of variables the same, with 8-bits you can only represent N^8 bits. (Of course, this argument works with any bit-size reduction, 256 and 8 aren't really special in any way.) And there's no way to keep the correspondence of sat/unsat partitioning of this space with fewer variables. The only way to keep satisfiability the same would be to correspondingly increase the number of variables, but that increase will be exponential as you can imagine, which beats the whole purpose of this reduction.
Having said that, bit-width reduction is a valid "heuristic" technique. The idea is simple: Take your original problem over 256-bits and treat all variables as if they are 8-bits. (Or even smaller if you like.)
If the reduced instance is SAT, take the model and see if that model also satisfies the original problem. (By simply interpreting the constants as is, since there's a direct injection.) If that's the case, you're done, you have a model for the original formula. If the reduced model does not satisfy the original problem, you can conclude nothing. (i.e., you can't conclude that the original problem is unsat or sat.) You can try to find a different model to try with in the reduced setting, or increase the bit-size, or give-up.
If the reduced instance is UNSAT, you can't conclude anything. (And this is the crucial bit.) You can increase the bit-size you reduce to, and try again.
The above algorithm is essentially how the non-linear integer solver works, for instance; by successively trying limited size approximations to it, and giving up after a certain number of tries if the iterations don't lead to a successful model. (And possibly switching to a different technique.) Note that this "trick" can never answer unsat, but it can find models. (See https://stackoverflow.com/a/13898524/936310 for details.)