summaryrefslogtreecommitdiff
path: root/compiler/SynthesizeSymbolic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SynthesizeSymbolic.ml')
-rw-r--r--compiler/SynthesizeSymbolic.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 5bcbd482..02b6e47c 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -155,3 +155,10 @@ let synthesize_assertion (v : V.typed_value) (e : expression option) =
let synthesize_forward_end (e : expression)
(el : expression T.RegionGroupId.Map.t) =
Some (ForwardEnd (e, el))
+
+let synthesize_loop (end_expr : expression option)
+ (loop_expr : expression option) : expression option =
+ match (end_expr, loop_expr) with
+ | None, None -> None
+ | Some end_expr, Some loop_expr -> Some (Loop { end_expr; loop_expr })
+ | _ -> raise (Failure "Unreachable")