diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
index 4d1c2f19dea..0a7bd7f11c3 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
@@ -4300,9 +4300,9 @@ let rec (norm :
                                   (rec_env, (lb.FStar_Syntax_Syntax.lbdef))))
                         (FStar_Pervasives_Native.snd lbs) memos in
                     let body_env =
-                      FStar_Compiler_List.fold_right
-                        (fun lb ->
-                           fun env2 ->
+                      FStar_Compiler_List.fold_left
+                        (fun env2 ->
+                           fun lb ->
                              let uu___5 =
                                let uu___6 =
                                  let uu___7 =
@@ -4313,9 +4313,13 @@ let rec (norm :
                                      uu___8, false) in
                                  Clos uu___7 in
                                (FStar_Pervasives_Native.None, uu___6) in
-                             uu___5 :: env2)
-                        (FStar_Pervasives_Native.snd lbs) env1 in
-                    norm cfg body_env stack2 body)
+                             uu___5 :: env2) env1
+                        (FStar_Pervasives_Native.snd lbs) in
+                    (FStar_TypeChecker_Cfg.log cfg
+                       (fun uu___6 ->
+                          FStar_Compiler_Util.print1
+                            "reducing with knot %s\n" "");
+                     norm cfg body_env stack2 body))
            | FStar_Syntax_Syntax.Tm_meta (head, m) ->
                (FStar_TypeChecker_Cfg.log cfg
                   (fun uu___3 ->
diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst
index b7cabc667fa..e3b7b7eb0c7 100644
--- a/src/typechecker/FStar.TypeChecker.Normalize.fst
+++ b/src/typechecker/FStar.TypeChecker.Normalize.fst
@@ -1628,8 +1628,11 @@ let rec norm : cfg -> env -> stack -> term -> term =
                     let rec_env = (None, Clos(env, fix_f_i, memo, true))::rec_env in
                     rec_env, memo::memos, i + 1) (snd lbs) (env, [], 0) in
             let _ = List.map2 (fun lb memo -> memo := Some (rec_env, lb.lbdef)) (snd lbs) memos in //tying the knot
-            let body_env = List.fold_right (fun lb env -> (None, Clos(rec_env, lb.lbdef, BU.mk_ref None, false))::env)
-                               (snd lbs) env in
+            // NB: fold_left, since the binding structure of lbs is that righmost is closer, while in the env leftmost
+            // is closer. In other words, the last element of lbs is index 0 for body, hence needs to be pushed last.
+            let body_env = List.fold_left (fun env lb -> (None, Clos(rec_env, lb.lbdef, BU.mk_ref None, false))::env)
+                               env (snd lbs) in
+            log cfg (fun () -> BU.print1 "reducing with knot %s\n" "");
             norm cfg body_env stack body
 
           | Tm_meta (head, m) ->
diff --git a/tests/bug-reports/Bug2849a.fst b/tests/bug-reports/Bug2849a.fst
new file mode 100644
index 00000000000..ce12ea7aae8
--- /dev/null
+++ b/tests/bug-reports/Bug2849a.fst
@@ -0,0 +1,18 @@
+module Bug2849a
+
+module T = FStar.Tactics
+
+let visit_terms (t: T.term): T.Tac unit =
+  let rec tm (t: T.term): T.Tac unit = match T.inspect_unascribe t with
+    | T.Tv_Match sc _ brs ->
+      // do work then recurse...
+      T.iter br brs;
+      tm sc
+    | _ -> ()
+  and br (b: T.branch): T.Tac unit = tm (snd b)
+  in tm t
+
+let nothing (): unit =
+  assert (true) by (
+    visit_terms (`true)
+  )
diff --git a/tests/bug-reports/Bug2849b.fst b/tests/bug-reports/Bug2849b.fst
new file mode 100644
index 00000000000..d5505e0a3f3
--- /dev/null
+++ b/tests/bug-reports/Bug2849b.fst
@@ -0,0 +1,28 @@
+module Bug2849b
+
+let pure () : int =
+  let rec f () : int = 1
+  and g () = 2
+  and h () = 3
+  in f ()
+
+let _ = assert_norm (pure () == 1)
+
+module T = FStar.Tactics
+
+let t1 () : T.Tac unit =
+  let rec f (): T.Tac unit = T.fail "fail_f"
+  and g () : T.Tac unit = ()
+  and h () : T.Tac unit = T.fail "fail_g"
+  in g ()
+
+let tac1 (): unit = assert (True) by (t1 ())
+
+let t2 () : T.Tac unit =
+  let rec f (): T.Tac unit = T.fail "fail_f"
+  and g () : T.Tac unit = ()
+  and h () : T.Tac unit = T.fail "fail_g"
+  in f ()
+
+[@@expect_failure]
+let tac2 (): unit = assert (True) by (t2 ())
diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
index 8efe0ecd990..d2e29a31f64 100644
--- a/tests/bug-reports/Makefile
+++ b/tests/bug-reports/Makefile
@@ -49,7 +49,8 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   Bug2552.fst Bug2597.fst Bug2471_B.fst Bug2605.fst Bug2614.fst Bug2622.fst \
   Bug2635.fst Bug2637.fst Bug2641.fst Bug1486.fst PropProofs.fst \
   Bug2684a.fst Bug2684b.fst Bug2684c.fst Bug2684d.fst Bug2659b.fst\
-  Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst
+  Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\
+  Bug2849a.fst Bug2849b.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst