Fix #1691 by bringing in GaloisInc/crucible#1004

intTests/test1691/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

intTests/test1691/test.c

@@ -0,0 +1,8 @@
+struct s {
+  unsigned x:1;
+  unsigned y:1;
+};
+
+int f(const struct s *ss) {
+  return ss->x == ss->y;
+}

intTests/test1691/test.saw

@@ -0,0 +1,17 @@
+enable_experimental;
+enable_lax_loads_and_stores;
+
+let f_spec = do {
+  ss <- llvm_alloc_readonly (llvm_alias "struct.s");
+  x <- llvm_fresh_var "x" (llvm_int 1);
+  y <- llvm_fresh_var "y" (llvm_int 1);
+  llvm_points_to_bitfield ss "x" (llvm_term x);
+  llvm_points_to_bitfield ss "y" (llvm_term y);
+
+  llvm_execute_func [ss];
+
+  llvm_return (llvm_term {{ if x == y then 1 else 0 : [32] }});
+};
+
+m <- llvm_load_module "test.bc";
+ov <- llvm_verify m "f" [] false f_spec (w4_unint_yices []);

intTests/test1691/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw