diff options
| author | Son Ho | 2022-11-08 21:50:07 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-10 11:35:30 +0100 |
| commit | a68926f574b23e75fe13ef3a500df7648a3c23d8 (patch) | |
| tree | 4439d56e6d049f537042020061d1cae96dd508d5 /compiler/SymbolicAst.ml | |
| parent | f8a394f0a11687f49bcd291e11f68244369e7f37 (diff) | |
Reorganize branching symbolic expansions to prepare for the join operation
Diffstat (limited to 'compiler/SymbolicAst.ml')
| -rw-r--r-- | compiler/SymbolicAst.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 39709a13..528d8255 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -67,6 +67,7 @@ type expression = | EndAbstraction of V.abs * expression | EvalGlobal of A.GlobalDeclId.id * V.symbolic_value * expression (** Evaluate a global to a fresh symbolic value *) + | Assertion of V.typed_value * expression (** An assertion *) | Expansion of mplace option * V.symbolic_value * expansion (** Expansion of a symbolic value. |