summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-25 12:25:23 +0100
committerSon Ho2022-01-25 12:25:23 +0100
commit039b84f49c8981955a079385357ccbc96d5aeb90 (patch)
tree131eb127eb014e1501304a7c0689298e84eb1c91 /src
parent73ef593adbefaddbb32ceac16c3ae05b277920af (diff)
Implement the forgotten Tuple case in SymbolicToPure.translate_expansion
Diffstat (limited to 'src')
-rw-r--r--src/SymbolicToPure.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index bae2925b..57f43b4e 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -457,7 +457,9 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
let field_proj = gen_field_proj fid in
Let (Assignment (var, field_proj), e))
id_var_pairs branch
- | T.Tuple -> raise Unimplemented
+ | T.Tuple ->
+ let vars = List.map (fun x -> Var x) vars in
+ Let (Deconstruct (vars, None, scrutinee), branch)
| T.Assumed T.Box ->
(* There should be exactly one variable *)
let var =