[nils-loose]

What changes

Z3 decides queries that mix Integer and bit-vector sorts very badly. A two-branch DCMP query that is UNSAT in 0.0 s over bit-vector constants stays unknown after minutes when the -1/0/1 result is int_to_bv(ite(..., 1, -1)). This PR makes the encoding consistent and keeps the semantics exact.

1. Comparison results over bit-vectors (executor).
   • DCMP/FCMP/LCMP and boolean-to-int now build their results as bit-vector ites.
   • Every Integer-to-bit-vector constructor (Int/Short/Byte/CharValue(…, IntegerFormula), int-to-FP casts) goes through the new BitvectorEncoding.toBitvector. It rebuilds numerals, ite, + - * and bv2int over bit-vectors, and keeps int_to_bv only where it cannot rewrite (string lengths, str.to_code, division).
   • The result equals int_to_bv in every model, because int_to_bv is a ring homomorphism mod 2^w.
   • This also covers the compare models in the String* classes without editing them.
2. String lengths and char codes (explorer, solver/Int2BvLifting.py).
   • Before each check, a bit-vector comparison between int_to_bv of a bounded Integer term and another such term becomes an Integer comparison.
   • Bounded terms are str.len, str.indexof, str.to_code, ubv_to_int, numerals, and + - * ite of those.
   • Where the range does not fit the width, the value keeps the wrap as an ite. Only char codes use a modulo. The rewrite is exact.
   • The ranges assume Java's string length bound of 2^31-1, and that bound is added to the query for each string the rewrite relied on.
   • If anything fails, the query is solved unchanged.
3. NaN and signed zeros (executor). With bit-vector results, the solver now picks NaN and -0.0 far more often, which exposed two imprecise models:
   • FCMPG/FCMPL returned a concrete result when an operand was NaN, and a symbolic result that ignored NaN. Their concrete result also used Float.compareTo, so -0.0 vs 0.0 gave -1 where the instructions give 0. They are now encoded like DCMP.
   • Double/Float.compare and Double/Float.compareTo share BitvectorEncoding.javaCompare, which follows the JDK: NaN equals itself and is greater than everything, and -0.0 < 0.0. The compareTo models had neither, which caused 2 regressions (divergences) before this fix.

Per-query solver timeout: I recommend leaving it off by default (no change in this PR).

• --solver-rlimit (Static pre-analysis pruning, with soundness fixes #65) only reorders the search: the last pending branch always runs unlimited, and nothing is given up on before MAX_RLIMIT.
• On the 23 runs that still have hard queries after this PR, --solver-rlimit 25000000 changed no verdict (0 points) and saved about 10% CPU.
• A query that runs out of its limit is never counted as UNSAT. Such a branch gets no unsat record, so it stays a candidate, and an undecided branch rules out SAFE (test_solver_rlimit).

Measurement

• Configuration: --sv-comp, 300 s CPU, 15 GB, no SA, compared with baseline-results.jsonl.
• Runs (1258):
  • all 149 KB runs with the causes of this item (int2bv-mixed-sort-encoding, string-char-int2bv-encoding-slow, string-length-int2bv-unbounded-query, solver-hard-query, no-solver-query-timeout, uf-global-constraints-unsliced, solver-query-growth-deep-unrolling);
  • 63 other baseline runs with slow queries (a query over 5 s, or killed while solving);
  • all 1046 baseline-correct runs.
• Result: +50 / -3, net +47, no new wrong verdict.
  • Affected set: +30.
  • Other slow runs: +22.
  • Regression set: -3 (1044 of 1046 still correct).
• CPU: 61055 s → 45024 s (-26%). On the regression set alone, 7673 s → 5941 s.
• Solver time on the 212 slow baseline runs (before → after):

	before	after
queries	3264	4798
total check time	11404 s	8206 s
median / p90 query	0.75 s / 4.4 s	0.00 s / 0.17 s
queries > 10 s	184	131
runs killed inside a query	99	48

task	prop	expected	base	new	Δ	CPU s
argv-tasks/AbstractChart_exceptionless	no-runtime-exception	SAFE	safe	timeout	-2	35 → 300
autostub/String_public_int_java_lang_String_lastIndexOf_java_lang_String	valid-assert	VIOLATION	violation	unknown	-1	4 → 3
argv-tasks/AbstractSerializationStreamReader_true	valid-assert	VIOLATION	timeout	violation	+1	300 → 11
argv-tasks/DiskBasedCache	valid-assert	VIOLATION	timeout	violation	+1	300 → 22
argv-tasks/MathHelper_true	valid-assert	VIOLATION	timeout	violation	+1	301 → 4
argv-tasks/ReverseInterpolator_false2	valid-assert	VIOLATION	timeout	violation	+1	302 → 22
autostub/Boolean_public_int_java_lang_Boolean_compareTo_java_lang_Boolean	valid-assert	VIOLATION	timeout	violation	+1	301 → 6
autostub/Float_public_short_java_lang_Float_shortValue	valid-assert	VIOLATION	timeout	violation	+1	302 → 5
float-nonlinear-calculation/Optimization2	valid-assert	VIOLATION	timeout	violation	+1	301 → 22
float-nonlinear-calculation/Optimization3	valid-assert	VIOLATION	timeout	violation	+1	302 → 112
float-nonlinear-calculation/coral32	valid-assert	VIOLATION	timeout	violation	+1	301 → 6
float-nonlinear-calculation/coral33	valid-assert	VIOLATION	timeout	violation	+1	301 → 80
float-nonlinear-calculation/coral52	valid-assert	VIOLATION	unknown	violation	+1	35 → 10
float-nonlinear-calculation/coral56	valid-assert	VIOLATION	timeout	violation	+1	301 → 232
float-nonlinear-calculation/coral61	valid-assert	VIOLATION	timeout	violation	+1	302 → 185
float-nonlinear-calculation/coral62	valid-assert	VIOLATION	timeout	violation	+1	302 → 182
float-nonlinear-calculation/coral79	valid-assert	VIOLATION	timeout	violation	+1	301 → 11
float-nonlinear-calculation/coral81	valid-assert	VIOLATION	timeout	violation	+1	302 → 22
argv-tasks/AbstractSerializationStreamReader_false	no-runtime-exception	SAFE	timeout	safe	+2	300 → 137
argv-tasks/AbstractSerializationStreamReader_true	no-runtime-exception	SAFE	timeout	safe	+2	301 → 140
argv-tasks/HotspotIntegerGenerator_false	no-runtime-exception	SAFE	timeout	safe	+2	302 → 97
argv-tasks/ImageRequest	valid-assert	SAFE	timeout	safe	+2	300 → 103
argv-tasks/Piecewise_true	no-runtime-exception	SAFE	unknown	safe	+2	111 → 37
argv-tasks/Piecewise_true	valid-assert	SAFE	unknown	safe	+2	125 → 37
argv-tasks/ReverseInterpolator_false	no-runtime-exception	SAFE	timeout	safe	+2	302 → 10
argv-tasks/ReverseInterpolator_false2	no-runtime-exception	SAFE	timeout	safe	+2	302 → 25
argv-tasks/SunTimes_true	no-runtime-exception	SAFE	timeout	safe	+2	300 → 7
argv-tasks/SunTimes_true	valid-assert	SAFE	timeout	safe	+2	302 → 7
float-nonlinear-calculation/Bessel	no-runtime-exception	SAFE	timeout	safe	+2	302 → 22
float-nonlinear-calculation/Bessel	valid-assert	SAFE	timeout	safe	+2	302 → 22
float-nonlinear-calculation/Optimization2	no-runtime-exception	SAFE	timeout	safe	+2	301 → 22
float-nonlinear-calculation/Optimization6	no-runtime-exception	SAFE	timeout	safe	+2	301 → 29
float-nonlinear-calculation/coral32	no-runtime-exception	SAFE	timeout	safe	+2	302 → 6
float-nonlinear-calculation/coral81	no-runtime-exception	SAFE	timeout	safe	+2	301 → 23
float-nonlinear-calculation/coral84	no-runtime-exception	SAFE	timeout	safe	+2	301 → 33

Notes on the flips:

• ProjectionGridRoundTripper_exceptionless (no-runtime-exception) became SAFE at 265 s, but timed out when re-run, so it is not counted.
• AbstractChart_exceptionless (no-runtime-exception) is confirmed on re-run. FCMP on NaN is now symbolic, so the search explores the NaN sides (25 rounds instead of 9), and the run times out on hard FP queries. Before, those sides were never explored. The old SAFE relied on that imprecision.
• String.lastIndexOf(String) (valid-assert) is model luck. The new model contains a surrogate pair, which does not survive the input round trip (divergence → UNKNOWN). That is an input-encoding issue, not this change.
• The 52 float_unboundedloop runs drop from about 100 s of solver time to about 0 s, but still time out on path explosion.

Tests

• Executor: new BitvectorEncodingTest.
  • Lowering at widths 8/16/32/64 is checked against int_to_bv under sampled assignments (a universal proof is exactly the kind of query Z3 hangs on).
  • The CMP results are checked against the old encoding.
  • javaCompare is checked against Double.compare/Float.compare on a grid that includes NaN, ±0 and ±∞.
  • ../gradlew test: 8761 tests, 0 failures.
• Explorer: new tests/test_int2bv_lifting.py.
  • 150 random comparison terms × 12 assignments keep their truth value, including supplementary chars and wrap boundaries.
  • It also covers overflow of length()+3, the signed bv2int pattern, and leaving pure bit-vector terms alone.
  • test_solver_rlimit, test_sa_walk and test_divergence pass.

Known limits

• Still unknown, quickly instead of a timeout: some string queries are hard for Z3's string theory itself, e.g. str.replace chains (Basic6: unknown, "max unfolding"). They now end UNKNOWN quickly instead of timing out.
• Encoding bug, not this item: indexOf(int) encodes the char as a decimal string (indexof-char-arg-encoded-as-decimal).
• Not done:
  • query slicing for trace-global UF constraints (uf-global-constraints-unsliced);
  • incremental solving (solver-query-growth-deep-unrolling);
  • nonlinear FP queries (solver-hard-query), which stay hard.
• No String model files touched: StringValue/StringBuilderValue/StringInvocation are unchanged. Their IntValue(…, IntegerFormula) calls benefit through the shared constructor.
• Possible conflict: fix/executor-small-bugs may also touch FCMP NaN handling.

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.