I want to set a constraint on a symbolic argument such that the final value never reaches a certain string. That is:

symArg = claripy.BVS('arg_1', 200) #The symbolic argument I have

#I want to set a constraint such that the value of
result = explorer.found[0].solver.eval(symArg, cast_to=bytes)
never contains the string "abcd"

I’ve been reading the document for days but, I’m unable to figure out how to do it. result is a byte type so, the constraint is result.replace(b'x80', b'') != "abcd" but, how do I tell it to Claripy? It seems like Claripy’s BitVector only allows bits and integer operations.

Any pointer would be helpful.