diff --git a/test/rust-val/AuxB.fsti b/test/rust-val/AuxB.fsti
new file mode 100644
index 00000000..5f2e4f03
--- /dev/null
+++ b/test/rust-val/AuxB.fsti
@@ -0,0 +1,3 @@
+module AuxB
+
+val bar : bool -> bool
diff --git a/test/rust-val/Makefile b/test/rust-val/Makefile
index a2d731ec..6e3d4436 100644
--- a/test/rust-val/Makefile
+++ b/test/rust-val/Makefile
@@ -56,9 +56,9 @@ $(CACHE_DIR)/%.checked: | .depend
 
 .PRECIOUS: %.rs
 %.rs: $(ALL_KRML_FILES) $(KRML_BIN)
-	$(KRML) -minimal -bundle $(notdir $(subst rust,Rust,$*))=\* \
+	$(KRML) -minimal -bundle AuxA+AuxB=[rename=Aux,rename-prefix] -bundle $(notdir $(subst rust,Rust,$*))=\* \
 	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
-	$(SED) -i 's/\(patterns..\)/\1\nmod auxa; mod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
+	$(SED) -i 's/\(patterns..\)/\1\nmod aux; mod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
 	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
 
 %.rust-test: %.rs
diff --git a/test/rust-val/Rusttest.fst b/test/rust-val/Rusttest.fst
index 4a1e5d17..5adc5ef5 100644
--- a/test/rust-val/Rusttest.fst
+++ b/test/rust-val/Rusttest.fst
@@ -9,7 +9,9 @@ let test2 (b: B.buffer bool) : HST.Stack bool
   (fun _ _ _ -> True)
 =
   let x = B.index b C._zero_for_deref in
-  AuxA.foo x
+  let r1 = AuxA.foo x in
+  let r2 = AuxB.bar x in
+  r1 && r2
 
 let main_ () : HST.Stack I32.t
   (fun _ -> True)
diff --git a/test/rust-val/auxa.rs b/test/rust-val/aux.rs
similarity index 81%
rename from test/rust-val/auxa.rs
rename to test/rust-val/aux.rs
index 9b6aa0ff..9a4f8903 100644
--- a/test/rust-val/auxa.rs
+++ b/test/rust-val/aux.rs
@@ -8,3 +8,8 @@ pub fn foo(x: bool) -> bool
 {
     return !x;
 }
+
+pub fn bar(x: bool) -> bool
+{
+    return x;
+}