diff --git a/intTests/test1703/Makefile b/intTests/test1703/Makefile
new file mode 100644
index 0000000000..f7abdbe50b
--- /dev/null
+++ b/intTests/test1703/Makefile
@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -emit-llvm -frecord-command-line -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc
diff --git a/intTests/test1703/test.bc b/intTests/test1703/test.bc
new file mode 100644
index 0000000000..cd5a518c33
Binary files /dev/null and b/intTests/test1703/test.bc differ
diff --git a/intTests/test1703/test.c b/intTests/test1703/test.c
new file mode 100644
index 0000000000..1727669f0c
--- /dev/null
+++ b/intTests/test1703/test.c
@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t weird(uint32_t cv[8], uint8_t i) {
+    return cv[i % 8];
+}
diff --git a/intTests/test1703/test.cry b/intTests/test1703/test.cry
new file mode 100644
index 0000000000..3bc9c7e1a6
--- /dev/null
+++ b/intTests/test1703/test.cry
@@ -0,0 +1,5 @@
+weird : [8][32] -> [8] -> [32]
+weird cv i = k
+    where
+        k = cvs @ i
+        cvs = cv # cvs
diff --git a/intTests/test1703/test.saw b/intTests/test1703/test.saw
new file mode 100644
index 0000000000..46915636e5
--- /dev/null
+++ b/intTests/test1703/test.saw
@@ -0,0 +1,15 @@
+import "test.cry";
+
+let weird_spec = do {
+  cv <- llvm_fresh_var "cv" (llvm_array 8 (llvm_int 32));
+  cv_p <- llvm_alloc (llvm_array 8 (llvm_int 32));
+  llvm_points_to cv_p (llvm_term {{ cv }});
+  i <- llvm_fresh_var "i" (llvm_int 8);
+
+  llvm_execute_func [cv_p, llvm_term i];
+
+  llvm_return (llvm_term {{ weird cv i }});
+};
+
+m <- llvm_load_module "test.bc";
+llvm_verify m "weird" [] false weird_spec (w4_unint_z3 []);
diff --git a/intTests/test1703/test.sh b/intTests/test1703/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test1703/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
index 9dc2bcb09b..979bb21af2 100644
--- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
@@ -314,8 +314,10 @@ lazyMux muxFn c tm fm =
       f <- fm
       muxFn c t f
 
--- selectV merger maxValue valueFn index returns valueFn v when index has value v
--- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger.
+-- @selectV merger maxValue valueFn vx@ treats @vx@ as an index, represented
+-- as a big-endian list of bits. It does a binary lookup, using @merger@ as an
+-- if-then-else operator. If the index is greater than @maxValue@, then it
+-- returns @valueFn maxValue@.
 selectV :: (SBool -> b -> b -> b) -> Natural -> (Natural -> b) -> SWord -> b
 selectV merger maxValue valueFn vx =
   case svAsInteger vx of
@@ -326,7 +328,13 @@ selectV merger maxValue valueFn vx =
   where
     impl _ x | x > maxValue || x < 0 = valueFn maxValue
     impl 0 y = valueFn y
-    impl i y = merger (svTestBit vx j) (impl j (y `setBit` j)) (impl j y) where j = i - 1
+    impl i y =
+      -- NB: `i` counts down in each iteration, so we use svTestBit (a
+      -- little-endian indexing function) to ensure that the bits are processed
+      -- in big-endian order. Alternatively, we could have `i` count up and use
+      -- svAt (a big-endian indexing function), but we use svTestBit as it is
+      -- slightly cheaper to compute.
+      merger (svTestBit vx j) (impl j (y `setBit` j)) (impl j y) where j = i - 1
 
 -- Big-endian version of svTestBit
 svAt :: SWord -> Int -> SBool
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index e5789d8525..9205af1b23 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -580,8 +580,10 @@ lazyMux muxFn c tm fm =
       f <- fm
       muxFn c t f
 
--- selectV merger maxValue valueFn index returns valueFn v when index has value v
--- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger.
+-- @selectV sym merger maxValue valueFn vx@ treats @vx@ as an index, represented
+-- as a big-endian list of bits. It does a binary lookup, using @merger@ as an
+-- if-then-else operator. If the index is greater than @maxValue@, then it
+-- returns @valueFn maxValue@.
 selectV :: forall sym b.
   Sym sym =>
   sym ->
@@ -595,7 +597,12 @@ selectV sym merger maxValue valueFn vx =
     impl _ x | x > maxValue || x < 0 = valueFn maxValue
     impl 0 y = valueFn y
     impl i y = do
-      p <- SW.bvAtBE sym vx (toInteger j)
+      -- NB: `i` counts down in each iteration, so we use bvAtLE (a
+      -- little-endian indexing function) to ensure that the bits are processed
+      -- in big-endian order. Alternatively, we could have `i` count up and use
+      -- bvAtBE (a big-endian indexing function), but we use bvAtLE as it is
+      -- slightly cheaper to compute.
+      p <- SW.bvAtLE sym vx (toInteger j)
       merger p (impl j (y `setBit` j)) (impl j y) where j = i - 1
 
 instance Show (SArray sym) where