From 15d90db02086f8ecae9a93ebf39c3c0ae8caa50f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 4 May 2022 15:39:05 +0200
Subject: Fix some issues when using states

---
 src/Translate.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/Translate.ml')

diff --git a/src/Translate.ml b/src/Translate.ml
index d69f1379..92261dba 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -232,8 +232,10 @@ let translate_function_to_pure (config : C.partial_config)
         let backward_sg =
           RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
         in
+        (* We need to ignore the forward inputs, and the state input (if there is) *)
         let _, backward_inputs =
-          Collections.List.split_at backward_sg.sg.inputs num_forward_inputs
+          Collections.List.split_at backward_sg.sg.inputs
+            (num_forward_inputs + if use_state_monad then 1 else 0)
         in
         (* As we forbid nested borrows, the additional inputs for the backward
          * functions come from the borrows in the return value of the rust function:
-- 
cgit v1.2.3