[Bug]: ReciprocityGuard Z3 solver always returns sat — dead `== True` check, every input passes as verified

[rahuldass19]

Description

QWED Version

0.1.0

Python Version

3.11.9

Which engine is affected?

ReciprocityGuard (US state tax withholding)

Input that caused the bug

from qwed_tax.jurisdictions.us.reciprocity_guard import ReciprocityGuard

guard = ReciprocityGuard()

# Any input — the solver is always sat
result = guard.verify_reciprocity(
    residence_state="NY",
    work_state="NJ",
    same_state=False,
)
print(result)
# → {"verified": True, ...} for EVERY input

Expected behavior

The guard should verify whether a state tax reciprocity agreement exists between the residence and work states, and whether the claimed withholding treatment is correct per that agreement.

• If a reciprocity agreement exists and the claimed treatment matches → verified=True
• If no reciprocity agreement exists → verified=False or UNVERIFIABLE
• If the claimed treatment contradicts the agreement → verified=False

Actual behavior

ReciprocityGuard returns verified=True for every input. The Z3 solver is always sat because the three rules together form a tautology — there is no input that makes the constraint system unsat.

Additionally, line 64 contains a dead code bug:

# reciprocity_guard.py line 64
if same_state == True or residence == work:

same_state is a Z3 BoolRef (line ~40-50). In Python, same_state == True constructs a Z3 expression (BoolRef), which is always truthy in an if statement. So the condition effectively reduces to just residence == work — the same_state check is dead code.

Root cause

reciprocity_guard.py lines 57-75:

if result == sat:
    if same_state == True or residence == work:
        # Same state — no reciprocity needed
        return {"verified": True, "message": "...same state..."}
    else:
        # Different states — check reciprocity
        return {"verified": True, "message": "...reciprocity verified..."}
else:
    return {"verified": False, "message": "Logic Error: No model found."}

The problem:

1. same_state == True is a Z3 expression, not a Python bool — always truthy in if
2. Both branches of the if/else return verified=True — there is no verified=False path except the unreachable "Logic Error" branch
3. The solver is always sat because the constraints don't actually test for reciprocity agreement existence — they just model the relationship between states

Why this is a bug

• The guard provides no real verification gate — every input passes
• An AI agent claiming "no withholding needed in NJ for NY resident" gets verified=True regardless of whether a reciprocity agreement actually exists
• The dead == True check means same_state parameter is ignored — caller's claim about same-state status is never evaluated

Severity

LOW — because State is enum-constrained upstream (only 8 states in models.py), the practical attack surface is limited. But the guard is structurally non-functional — it's a pass-through masquerading as a verifier.

Fix direction

1. Fix the dead Z3 comparison: Replace same_state == True with is_true(same_state) from z3 (proper Z3 bool evaluation), or restructure to not pass same_state as a Z3 variable
2. Add reciprocity agreement data: The guard needs a table of actual reciprocity agreements (e.g., NY-NJ has reciprocity, NY-PA does not) to verify against — currently it models the relationship but not the agreement
3. Add fail-closed paths: Unknown state pairs → verified=False (intersects with [Bug]: Unknown, unsupported, or partially modeled tax rules are treated as verified #16 — unknown rules treated as verified)
4. Return verified=False when no reciprocity exists: The else branch should not default to verified=True

Suggested regression tests

# Same state — no reciprocity needed
assert guard.verify_reciprocity("NY", "NY", same_state=True)["verified"] == True

# Known reciprocity pair — verified
assert guard.verify_reciprocity("NJ", "PA", same_state=False)["verified"] == True

# No reciprocity — blocked
assert guard.verify_reciprocity("NY", "TX", same_state=False)["verified"] == False

# Unknown state pair — fail-closed (not verified)
assert guard.verify_reciprocity("CA", "FL", same_state=False)["verified"] == False

Related issues

• [Bug]: Unknown, unsupported, or partially modeled tax rules are treated as verified #16 (unknown rules → verified): This guard's always-pass behavior is a variant of the "no rule found → verified" pattern — the reciprocity rule table is effectively empty
• [Bug]: Verification outputs overstate assurance by returning success without comparing a claim to the computed truth #18 (success without comparing claim): The guard never compares a claimed withholding treatment against the computed reciprocity result