Now, we use raw Z3 solver (without unrolling) for rewriter, and the bug is gone away (I still don't know why, BUT ... who care ;) )