String modes

String is the one type where the model choice changes how fast a proof solves. Set it per proof with @BmcProof(stringMode = ...), or project-wide in the plugin config.

REFINEMENT (default)

The engine’s string solver is on, so content operations like equals, contains, and substring are reasoned end to end. Symbolic input strings are bounded by maxStringLength. Use this when the proof is about what a string contains.

CHAR_ARRAY_MODEL

String becomes a plain char-array model with the string solver off. Use this when the proof treats strings as data and moves bytes around: encoding into buffers, byte and char conversion, number formatting. In those cases the string solver is usually the bottleneck, and turning it off can be the difference between a fast proof and a timeout. A content operation the simpler model can’t decide comes back Unknown rather than wrong.

Rule of thumb: proving something about string content, stay on REFINEMENT. Pushing string data through code, try CHAR_ARRAY_MODEL.