diff --git a/Makefile b/Makefile
index 24b9d2bd4a..8f456d8c3d 100644
--- a/Makefile
+++ b/Makefile
@@ -144,15 +144,6 @@ OUTPUT_PREOUTS := \
 	Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs \
 	Crypto.UnsaturatedSolinasHeuristics.Tests.get_balances
 
-ifneq ($(SKIP_BEDROCK2),1)
-OUTPUT_VOS += \
-	src/Bedrock/Group/ScalarMult/LadderStep.vo \
-	src/Bedrock/Group/ScalarMult/MontgomeryLadder.vo
-OUTPUT_PREOUTS += \
-	Crypto.Bedrock.Group.ScalarMult.LadderStep.ladderstep_body \
-	Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body
-endif
-
 CHECK_OUTPUTS := $(addprefix check-,$(OUTPUT_PREOUTS))
 ACCEPT_OUTPUTS := $(addprefix accept-,$(OUTPUT_PREOUTS) fiat-amd64.test)
 
diff --git a/output-tests/Crypto.Bedrock.Group.ScalarMult.LadderStep.ladderstep_body.expected b/output-tests/Crypto.Bedrock.Group.ScalarMult.LadderStep.ladderstep_body.expected
deleted file mode 100644
index 91438f1249..0000000000
--- a/output-tests/Crypto.Bedrock.Group.ScalarMult.LadderStep.ladderstep_body.expected
+++ /dev/null
@@ -1,32 +0,0 @@
-ladderstep_body = 
-fun (width : Z) (BW : Bitwidth width) (word : word width) (mem : map.map word byte) (word_ok : word.ok word) (mem_ok : map.ok mem)
-  (field_parameters : FieldParameters) (field_representaton : FieldRepresentation) =>
-(["X1"; "X2"; "Z2"; "X3"; "Z3"], [],
-noreassign
-  (noskips
-     (cmd.stackalloc "A" size_in_bytes
-        (cmd.seq (cmd.call [] add ["A"; "X2"; "Z2"])
-           (cmd.seq (cmd.call [] sub ["X2"; "X2"; "Z2"])
-              (cmd.seq (cmd.call [] add ["Z2"; "X3"; "Z3"])
-                 (cmd.seq (cmd.call [] sub ["Z3"; "X3"; "Z3"])
-                    (cmd.seq (cmd.call [] mul ["Z3"; "Z3"; "A"])
-                       (cmd.seq (cmd.call [] mul ["Z2"; "Z2"; "X2"])
-                          (cmd.seq (cmd.call [] square ["A"; "A"])
-                             (cmd.seq (cmd.call [] square ["X2"; "X2"])
-                                (cmd.stackalloc "E" size_in_bytes
-                                   (cmd.seq (cmd.call [] sub ["E"; "A"; "X2"])
-                                      (cmd.seq (cmd.call [] add ["X3"; "Z3"; "Z2"])
-                                         (cmd.seq (cmd.call [] square ["X3"; "X3"])
-                                            (cmd.seq (cmd.call [] sub ["Z3"; "Z3"; "Z2"])
-                                               (cmd.seq (cmd.call [] square ["Z3"; "Z3"])
-                                                  (cmd.seq (cmd.call [] mul ["Z3"; "X1"; "Z3"])
-                                                     (cmd.seq (cmd.call [] mul ["X2"; "A"; "X2"])
-                                                        (cmd.seq (cmd.call [] scmula24 ["Z2"; "E"])
-                                                           (cmd.seq (cmd.call [] add ["Z2"; "A"; "Z2"])
-                                                              (cmd.seq (cmd.call [] mul ["Z2"; "E"; "Z2"])
-                                                                 (fold_right (fun (v : string) (c : Syntax.cmd) => cmd.seq (cmd.unset v) c)
-                                                                    cmd.skip [])))))))))))))))))))))))
-     : forall (width : Z) (BW : Bitwidth width) (word : word width) (mem : map.map word byte),
-       word.ok word -> map.ok mem -> forall field_parameters : FieldParameters, FieldRepresentation -> Syntax.func
-
-Arguments ladderstep_body {width}%Z_scope {BW word mem word_ok mem_ok field_parameters field_representaton}
diff --git a/output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected b/output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected
deleted file mode 100644
index efc4eed0f2..0000000000
--- a/output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected
+++ /dev/null
@@ -1,32 +0,0 @@
-     = ("montladder",
-       (["OUT"; "K"; "U"], [],
-       noreassign
-         (noskips
-            (cmd.stackalloc "X1" size_in_bytes
-               (cmd.seq (cmd.call [] from_word ["X1"; 1])
-                  (cmd.stackalloc "Z1" size_in_bytes
-                     (cmd.seq (cmd.call [] from_word ["Z1"; 0])
-                        (cmd.stackalloc "X2" size_in_bytes
-                           (cmd.seq (cmd.call [] felem_copy ["X2"; "U"])
-                              (cmd.stackalloc "Z2" size_in_bytes
-                                 (cmd.seq (cmd.call [] from_word ["Z2"; 1])
-                                    (cmd.seq (cmd.set "swap" (word.unsigned (word.b2w false)))
-                                       (cmd.seq (cmd.set "_gs_i0" (word.unsigned (word.of_Z (Z.of_nat 253))))
-                                          (cmd.seq
-                                             (cmd.while (expr.op bopname.ltu 0 "_gs_i0")
-                                                (cmd.seq (cmd.set "_gs_i0" (expr.op bopname.sub "_gs_i0" 1))
-                                                   (cmd.seq
-                                                      (cmd.set "s_i"
-                                                         (expr.op bopname.and
-                                                            (expr.op bopname.sru
-                                                               (expr.load access_size.one (expr.op bopname.add "K" (expr.op bopname.sru "_gs_i0" 3)))
-                                                               (expr.op bopname.and "_gs_i0" 7)) 1))
-                                                      (cmd.seq (cmd.set "swap" (expr.op bopname.xor "swap" "s_i"))
-                                                         (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "X1"; "X2"])
-                                                            (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "Z1"; "Z2"])
-                                                               (cmd.seq (cmd.call [] "ladderstep" ["U"; "X1"; "Z1"; "X2"; "Z2"])
-                                                                  (cmd.seq (cmd.set "swap" "s_i") (cmd.seq (cmd.unset "s_i") cmd.skip)))))))))
-                                             (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "X1"; "X2"])
-                                                (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "Z1"; "Z2"])
-                                                   (cmd.seq (cmd.call [] "fe25519_inv" ["OUT"; "Z1"]) (cmd.seq (cmd.call [] mul ["OUT"; "X1"; "OUT"]) cmd.skip))))))))))))))))))
-     : string * func