diff options
| author | Son Ho | 2022-01-06 15:31:05 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-06 15:31:05 +0100 |
| commit | 973e14973ca857ed0b3fd69fa45901c8ae08820e (patch) | |
| tree | 5a8bda663f788ec7df203c6b42f539df1421c48d /src/InterpreterExpansion.ml | |
| parent | a263101a71d5be9d3f2a738527c2eedc850eb9ad (diff) | |
Fix some issues when evaluating assertions
Diffstat (limited to 'src/InterpreterExpansion.ml')
| -rw-r--r-- | src/InterpreterExpansion.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 46398c84..7366a819 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -166,6 +166,8 @@ let replace_symbolic_values (at_most_once : bool) (** Apply a symbolic expansion to a context, by replacing the original symbolic value with its expanded value. Is valid only if the expansion is not a borrow (i.e., an adt...). + + This function does update the synthesis. *) let apply_symbolic_expansion_non_borrow (config : C.config) (original_sv : V.symbolic_value) (expansion : symbolic_expansion) |