summaryrefslogtreecommitdiff
path: root/compiler/SymbolicAst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SymbolicAst.ml')
-rw-r--r--compiler/SymbolicAst.ml1
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.