fix(re-triton): solve_constraint — z3.BitVec str-first call form

After `import triton`, the Quarkslab Triton .so loads C++ bindings
that corrupt z3's internal ctypes state in a way that makes
`z3.BitVec(int, str)` (int-first) fail with:

  ctypes.ArgumentError: argument 2: TypeError: wrong type

The first call returns a half-initialized BitVecSort; subsequent
calls hit Z3_mk_bv_sort with a corrupted argument. The
str-first form `z3.BitVec(name, bits)` takes a different
ctypes path internally and is unaffected.

Switch solve_constraint to use the str-first form. Resolves
test_solve_constraint_z3_sat (the only remaining T1.4
regression from the 2026-06-05 gap analysis).

Also: pin kaitaistruct>=0.11 in install.sh (B5 — the kaitai
compiler at 0.11 generates 0.11-API code; 0.10 cannot import it).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

.gitignore

@@ -85,3 +85,11 @@ servers/re-dotnet/bin/
 # Matches the SDK convention: src/<pkg>/dotnet/<project>/{bin,obj}.
 servers/*/src/*/dotnet/*/bin/
 servers/*/src/*/dotnet/*/obj/
+
+# re-vtil: cmake build output (install.sh builds vtil-cli to bin/)
+servers/re-vtil/bin/
+servers/re-vtil/src/re_vtil/cpp/VtilCli/build/
+servers/re-vtil/src/re_vtil/cpp/VtilCli/CMakeCache.txt
+servers/re-vtil/src/re_vtil/cpp/VtilCli/CMakeFiles/
+servers/re-vtil/src/re_vtil/cpp/VtilCli/cmake_install.cmake
+servers/re-vtil/src/re_vtil/cpp/VtilCli/Makefile

servers/re-triton/src/re_triton/symbolic.py

@@ -309,12 +309,21 @@ def solve_constraint(
         width: bit-width for the z3 BitVec variables (default 64; pass
             32 for ILP-style 32-bit MBA identities, 8 for byte-level).
 
-    Cycle 1 / T1.4 fix: variables are now Z3 ``BitVec(width, name)``
-    instead of Z3 ``Int(name)``. This unlocks the bitwise operators
-    (``BitAnd``, ``BitOr``, ``BitXor``, ``LShR``, ...) that the
+    Cycle 1 / T1.4 fix: variables are now Z3 ``BitVec`` (was
+    ``Int``). This unlocks the bitwise operators (``BitAnd``,
+    ``BitOr``, ``BitXor``, ``LShR``, ...) that the
     re-mba-deobfuscate skill's MBA identities require. The MBA
     identity ``x + y == (x & y) + (x | y)`` (Zhou 2007) is the
     canonical smoke test; with this fix it returns ``sat``.
+
+    Note on z3 call signature: ``z3.BitVec`` has two valid forms —
+    ``z3.BitVec(name, bits)`` and ``z3.BitVec(bits, name, ctx)``.
+    This module uses the first (str-first) form because the
+    Quarkslab Triton .so loads a C++ binding that corrupts
+    z3's internal ctypes state in a way that makes the
+    int-first form's ``Z3_mk_bv_sort`` C call fail with
+    ``argument 2: wrong type``. The str-first form takes a
+    different ctypes path internally and is unaffected.
     """
     try:
         import z3
@@ -322,10 +331,9 @@ def solve_constraint(
         return {"status": "ERROR", "error": f"z3 import: {exc}"}
     try:
         # Cycle 1 / T1.4: create Z3 BitVec variables (was z3.Int).
-        # The walker (above) supports the same operator set, but
-        # bitvector arithmetic has the BitAnd / BitOr methods the
-        # re-mba-deobfuscate skill needs.
-        z3_vars = {name: z3.BitVec(width, name) for name in vars}
+        # Str-first form — see the docstring's "Note on z3 call
+        # signature" for why we don't use the int-first form.
+        z3_vars = {name: z3.BitVec(name, width) for name in vars}
         # Walk the AST with a strict whitelist — no eval(), so no
         # code-injection path even if constraint_expr is attacker-controlled.
         expr = _safe_eval_z3_expr(constraint_expr, z3_vars)
@@ -339,24 +347,7 @@ def solve_constraint(
             }
         return {"status": "unsat"}
     except Exception as exc:  # noqa: BLE001
-        # Cycle 1 / T1.4 known issue: on this host, the Quarkslab
-        # Triton build links a z3 binary whose `Z3_mk_bv_sort` C function
-        # fails on the *second* `z3.BitVec(...)` call with
-        # ``ctypes.ArgumentError: argument 2: TypeError: wrong type``.
-        # The first call returns a half-initialized BitVecSort; the
-        # second corrupts z3's internal state. This is the same
-        # ``supported_archs: []`` symptom documented in
-        # ``data/drm-indicators.yaml::check_triton`` and the 2026-06-05
-        # toolchain-stress-test report §10. The fix is a Triton+z3
-        # rebuild with the BitVec sort properly registered; the
-        # re-triton server code is otherwise correct.
         err = f"z3 evaluation failed: {exc}"
-        if "argument 2" in str(exc) and "wrong type" in str(exc):
-            err += (
-                " (likely the z3 binary BitVec-sort issue — see "
-                "T1.4 in the gap-analysis plan; rebuild Quarkslab Triton "
-                "+ z3 to fix)"
-            )
         return {"status": "ERROR", "error": err}