Make a constraint more difficult to solve for a constraint solver?

I am a newbie to SMT solving and I am writing to inquire some advice and pointers to understand what is a really difficult constraint for SMT solver to solve, for instance Z3.

I tried to tweak the length of bit vectors, for instance in the following way:

>>> a = BitVec("a", 10000)
>>> b = BitVec("b", 10000)
>>> c = a >> 18 + 6 - 32 + 69 == b <<12 + 7 * 32
>>>
>>> s = Solver()
>>> s.add(c)
>>> s.check()

While intuitively this could leads to a quite large search space, it turns out that Z3 still does a pretty good job and solve it swiftly.

I am aware that some crypto hash functions or math formulas (e.g., Collatz conjecture) could make constraint solving quite difficult. But that seems pretty extreme. On the other hand, for instance suppose I have the following constraint:

a * 4 != b + 5

How can I make it more difficult for a constraint solver to solve? Is there any general way of doing so? I got the impression that somehow it a constraint turns to be "non-linear", then it is difficult. But it is still unclear to me how that works.

=================================

Thank you for all the kind notes and insightful posts. I appreciate it very much!

So here are some tentative tests according to @usr's suggestion:

c = BitVec("c", 256)

for i in range(0, 10):
    c = c ^ (c << 13) + 0x51D36335;

s = Solver()
s.add(c == 0xdeadbeef)
print (s.check())
print (s.model())


➜  work time python test.py
sat
[c = 37865234442889991147654282251706833776025899459583617825773189302332620431087]
python test.py  0.38s user 0.07s system 81% cpu 0.550 total

Bitvector logic is always decidable; so while things may take long, z3 can solve all bitvector problems. Of course, if the bit-vector sizes involved are large, then the solver can take extremely long, or run out of memory before finding a solution. Multiplication and crypto-algorithms are typical examples that always cause a hard time as the bit sizes increase.

On the flip side, we have non-linear integer problems. There's no decision procedure for them, and while z3 "tries its best," such problems are typically beyond scope for theoretical reasons. You can find many instances of these in stack-overflow posts. Here's a most recent one: Z3 returns model not available