summaryrefslogtreecommitdiff
path: root/compiler/InterpreterBorrows.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterBorrows.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 4d67a4e4..e97795a1 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -452,7 +452,8 @@ let give_back_symbolic_value (_config : C.config)
| V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
->
()
- | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate ->
+ | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate
+ | ConstGeneric | TraitConst ->
raise (Failure "Unreachable"));
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in