summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterBorrows.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index ccd41747..bc5341c5 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -432,7 +432,7 @@ let give_back_symbolic_value (_config : C.config)
| V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
| V.FunCallRet | V.SynthInput -> failwith "Unrechable");
(* Store the given-back value as a meta-value for synthesis purposes *)
- let mv = mk_typed_value_from_symbolic_value nsv in
+ let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
let subst (_abs : V.abs) local_given_back =
(* Compute the projection over the given back value *)