summaryrefslogtreecommitdiff
path: root/src/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/SymbolicToPure.ml')
-rw-r--r--src/SymbolicToPure.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 4fa8e54c..8b31bffa 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1246,10 +1246,6 @@ and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
let e = translate_expression e ctx in
let meta =
match meta with
- | S.Aggregate (p, rv) ->
- let p = translate_opt_mplace p in
- let rv = typed_value_to_rvalue ctx rv in
- Aggregate (p, rv)
| S.Assignment (p, rv) ->
let p = translate_mplace p in
let rv = typed_value_to_rvalue ctx rv in