I want to factor a number n with Bitvectors in Z3. I use Bitvectores because I want to constrain single bits in p an q. This simple example does work and the solver returns "sat".
from z3 import *
Bits = 32
n = 12
p_vec = BitVec('p', Bits)
q_vec = BitVec('q', Bits)
n_vec = BitVecVal(n,Bits)
s = Solver()
s.add(p_vec * q_vec == n_vec)
s.add(p_vec > 1, q_vec > 1)
s.add(BVMulNoOverflow(p_vec,q_vec,False))
print (s.check())
But now I want to factor another number n with 4096 Bits. So I changend Bits=4096 in the example and used the same numbers. The solver give me now "unknow" instead of "sat". It seems the solver discontinues at some point. Do I have to change some solver settings or is there an other approach to do that.
When I run your program with Bits = 4096, it does not say unknown. It simply does not finish quickly (I waited for a few minutes), and I wouldn't expect it to.
Bitvector solver is complete. That is, if you wait long enough, it'll eventually return sat or unsat, assuming you do not run out of memory (and patience). For this problem, however, the amount you'll wait might be practically infinite, and you'll most likely run out of memory on your computer long before that happens. So, I'm not sure how you're getting that unknown. Maybe you're using some timeout options, or something else you're not showing here.
You can try adding constraints of the form: p_vec < n and q_vec < p_vec to break symmetries. And it could indeed help in some cases since n is a constant. But this is in general futile, and for any reasonable bit size for use in cryptographic practice, the solver will practically loop forever.
Factorization is a hard problem for obvious reasons and an SMT solver is definitely not the right tool for it. See here for an earlier discussion: Bitvector function Z3