[nils-loose]

Int2BvLifting takes str.to_code in [-1, 0x10FFFF] (Z3's char range), so a lifted charAt comparison needs a (t + 32768) mod 65536 - 32768-style wrap, which makes Z3 slow on char-code queries.

Changes

• The executor encodes a Java string with one SMT char per UTF-16 unit. For queries in which every char the query itself introduces is a Java char (java_chars_only), char codes are lifted with range [-1, 0xFFFF], which needs no mod.
• lift_query adds str.to_code(x) <= 0xFFFF for each char code the rewrite relied on (as it already does for string lengths), so the lifted query is equivalent to the original one under these bounds and its models are models of the original.
• java_chars_only (iterative, memoised) rejects a query if a string constant (incl. regex range endpoints) has a char above 0xFFFF, if a str.from_code argument's range exceeds 0xFFFF, or if it contains a Char-sorted term or a quantifier. Such queries keep the previous full-range lifting (separate cached instance).
• Not done: simply setting MAX_CHAR_CODE = 0xFFFF. That is not sound in general:
  • string literals with surrogate pairs: JavaSMT's makeString iterates code points, so "😀" becomes one SMT char \u{1f600} (StringValue.java:48, a separate pre-existing encoding issue);
  • str.from_code of an int code point (StringValue.codePointString, indexOf(int));
  • the executor's per-string BMP bound (StringValue.getBounds) is only added for registered inputs, not for symbolic returns/fields or String[] elements.

Soundness

Take any Java execution of the path and assign each SMT string variable the UTF-16 units of its Java value (this is the executor's model of charAt = to_code(str.at)). Under the guard, every char in the query comes from such a variable, from a constant <= 0xFFFF, from str.from_code of an argument <= 0xFFFF (with to_code taken as <= 0xFFFF by induction over the term) or from str.from_int digits; every other string operation only copies chars. So that assignment satisfies every added bound, and the bounds exclude only models no Java execution can realise. The argument does not depend on the executor's input bound. Retry constraints (extra_exprs) are not lifted and only remove models, as before.

Measured

• 108 recorded char-code queries (securibench, java-ranger, jbmc; Z3 5.3.1, seed 0, 60 s cap): solver CPU 759 s -> 257 s, unsolved 5 -> 2 (some queries are slower on some seeds; timings are heavy-tailed). LoopCharAt core: timeout -> 0.04 s.
• Of 748 recorded queries only 3 (indexOf(int)) fall back to the full-range lifting.
• A/B on 10 string tasks: identical verdicts; on timeouts more solver calls finish within the CPU limit.
• Tests: 6 new tests in tests/test_int2bv_lifting.py (lift equivalence under BMP and supplementary assignments, incl. a mutation-checked test that fails without the added bound; guard cases; selection in lift_int2bv). Explorer suite: 212 passed (dev: 200 passed, 6 skipped).

Full-campaign numbers follow in a comment.

🤖 Generated with Claude Code

[nils-loose]

Full campaign: 1713 SV-COMP jobs (300 s CPU, no SA, sv-comp.cfg, 15 GB / -Xmx12g), dev 209cc0e and svcomp27/overnight-solver-perf (dev + #96 + #98 + #99) run at the same time, 16 slots x 2 cores each.

	dev	dev + #96 + #98 + #99
points	2192	2201 (+9)
correct SAFE / VIOLATION	804 / 664	804 / 673
wrong (5 known wrong labels, #63)	5	5
new wrong verdicts		0
timeouts / UNKNOWN	136 / 103	127 / 103
CPU sum	46431 s	40090 s (-14%)

Attribution: the 20 runs that changed were re-run with each change switched off (--no-fp-tactic, --no-executor-cds, without #99).

This PR: no verdict changes (without it, the 20 changed runs give the same verdicts). CPU on runs with the same decided verdict, combined with #96: securibench -16%, autostub -19%, java-ranger-regression -44%; not separated from #96.

🤖 Generated with Claude Code