Python -> Laurel translation: unmodeled method calls to havoc non-receiver arguments too

Strata/Languages/Python/PythonToLaurel.lean

@@ -1138,7 +1138,17 @@ private def mkHavocStmtsForUnmodeledCall (ctx : TranslationContext)
         | _ => false)
     let heapHavoc := if !involveHeap then [] else
         [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar "$heap"] (mkStmtExprMd (.Hole false none))) md]
-    [mkStmtExprMd $ .Block (holeExceptHavoc ++ calleeHavoc ++ heapHavoc) none]
+    -- Havoc local arguments: the unmodeled call may have side effects on
+    -- its arguments (e.g., iterating over an iterable argument).
+    let argHavoc := inputExprs.flatMap fun inputExpr =>
+        if let .Name _ n _ := inputExpr then
+          match ctx.variableTypes.find? (λ v => Prod.fst v == n.val) with
+          | some (varName, ty) =>
+            if isCompositeType ctx ty then []
+            else [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar varName] (mkStmtExprMd (.Hole false none))) md]
+          | _ => []
+        else []
+    [mkStmtExprMd $ .Block (holeExceptHavoc ++ calleeHavoc ++ argHavoc ++ heapHavoc) none]
   else []
 
 partial def translateAssign  (ctx : TranslationContext)

StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected

@@ -4,5 +4,6 @@ test_havoc_callee_after_hole_call.py(17, 0): ❓ unknown - expected unknown beca
 test_havoc_callee_after_hole_call.py(21, 0): ✅ pass - expected pass nothing should be havocked
 test_havoc_callee_after_hole_call.py(23, 0): ✅ pass - callElimAssert_requires_5
 test_havoc_callee_after_hole_call.py(26, 0): ❓ unknown - expected unknown because heap should be havocked
-DETAIL: 2 passed, 0 failed, 4 inconclusive
+test_havoc_callee_after_hole_call.py(31, 0): ❓ unknown - expected unknown because argument locals should be havocked
+DETAIL: 2 passed, 0 failed, 5 inconclusive
 RESULT: Inconclusive

StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py

@@ -24,3 +24,8 @@ def __init__(self, n: int):
 a.val = 1
 some_unmodeled_call_6(a)
 assert a.val == 1, "expected unknown because heap should be havocked" 
+
+xs2: list[int] = [1, 2]
+ys: list[int] = []
+xs2.unknown_method_that_may_modify_arguments(ys)
+assert ys == [], "expected unknown because argument locals should be havocked"