summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Translate.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 221d4e73..54e24066 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -216,11 +216,15 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
(* We need to ignore the forward inputs, and the state input (if there is) *)
let backward_inputs =
let sg = backward_sg.sg in
+ (* TODO: *)
+ assert (not !Config.return_back_funs);
(* We need to ignore the forward state and the backward state *)
let num_forward_inputs =
- sg.info.num_fwd_inputs_with_fuel_with_state
+ sg.info.fwd_info.num_inputs_with_fuel_with_state
+ in
+ let num_back_inputs =
+ (Option.get sg.info.back_info).num_inputs_no_fuel_no_state
in
- let num_back_inputs = Option.get sg.info.num_back_inputs_no_state in
Collections.List.subslice sg.inputs num_forward_inputs
(num_forward_inputs + num_back_inputs)
in