diff options
Diffstat (limited to 'compiler/SynthesizeSymbolic.ml')
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 504fcdb5..c74a831e 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -155,3 +155,6 @@ let synthesize_assignment (lplace : mplace) (rvalue : V.typed_value) match expr with | None -> None | Some expr -> Some (Meta (Assignment (lplace, rvalue, rplace), expr)) + +let synthesize_assertion (v : V.typed_value) (expr : expression option) = + match expr with None -> None | Some expr -> Some (Assertion (v, expr)) |