diff --git a/heapster-saw/examples/Makefile b/heapster-saw/examples/Makefile
index 3215b3ab7e..25980f49fe 100644
--- a/heapster-saw/examples/Makefile
+++ b/heapster-saw/examples/Makefile
@@ -16,22 +16,29 @@ ifeq ($(SAW),)
   endif
 endif
 
+# If running in GitHub Actions, the $CI environment variable will be defined
+# (see https://docs.github.com/en/actions/learn-github-actions/variables#default-environment-variables)
+# and these Makefile rules will not be defined. As a consequence, Make will
+# /never/ rebuild .bc files. This ensures that the CI will always test the .bc
+# files that were checked into version control. (See #1801 for an example of
+# what can go wrong if CI rebuilds .bc files with different compilers from what
+# were used to originally produce them.)
 ifeq ($(CI),)
   %.bc: %.c
 	clang -emit-llvm -g -c $<
-endif
-
-%_gen.v: %.saw %.bc
-	$(SAW) $<
 
-xor_swap_rust.bc: xor_swap_rust.rs
+  xor_swap_rust.bc: xor_swap_rust.rs
 	rustc --crate-type=lib --emit=llvm-bc xor_swap_rust.rs
 
-rust_data.bc: rust_data.rs
+  rust_data.bc: rust_data.rs
 	rustc --crate-type=lib --emit=llvm-bc rust_data.rs
 
-rust_lifetimes.bc: rust_lifetimes.rs
+  rust_lifetimes.bc: rust_lifetimes.rs
 	rustc --crate-type=lib --emit=llvm-bc rust_lifetimes.rs
+endif
+
+%_gen.v: %.saw %.bc
+	$(SAW) $<
 
 # Lists all the Mr Solver tests, without their ".saw" suffix
 MR_SOLVER_TESTS = # arrays_mr_solver linked_list_mr_solver sha512_mr_solver