diff --git a/intTests/test0220/Makefile b/intTests/test0220/Makefile
new file mode 100644
index 000000000..2eef228fd
--- /dev/null
+++ b/intTests/test0220/Makefile
@@ -0,0 +1,18 @@
+# The current checked-in test.bc was generated by:
+#    Apple clang version 15.0.0 (clang-1500.1.0.2.5)
+#    Target: arm64-apple-darwin22.6.0
+#    Thread model: posix
+#    InstalledDir: /Library/Developer/CommandLineTools/usr/bin
+# but neither the target nor the clang/llvm version is expected to be
+# significant.
+CC = clang
+CFLAGS = -g -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc
diff --git a/intTests/test0220/test.bc b/intTests/test0220/test.bc
new file mode 100644
index 000000000..dce5cf641
Binary files /dev/null and b/intTests/test0220/test.bc differ
diff --git a/intTests/test0220/test.c b/intTests/test0220/test.c
new file mode 100644
index 000000000..dd39df9ea
--- /dev/null
+++ b/intTests/test0220/test.c
@@ -0,0 +1,5 @@
+unsigned char y;
+
+void f(void) {
+   y = 6;
+}
diff --git a/intTests/test0220/test.saw b/intTests/test0220/test.saw
new file mode 100644
index 000000000..0d8be0cb6
--- /dev/null
+++ b/intTests/test0220/test.saw
@@ -0,0 +1,15 @@
+// Test an inexact postcondition.
+
+mod <- llvm_load_module "test.bc";
+
+let spec = do {
+   llvm_alloc_global "y";
+   y <- llvm_fresh_var "y" (llvm_int 8); 
+   llvm_points_to (llvm_global "y") (llvm_term y); 
+   llvm_execute_func [];
+   y_new <- llvm_fresh_var "y_new" (llvm_int 8);
+   llvm_points_to (llvm_global "y") (llvm_term y_new);
+   llvm_postcond {{ y_new > 0 }};
+};
+
+llvm_verify mod "f" [] false spec abc;
diff --git a/intTests/test0220/test.sh b/intTests/test0220/test.sh
new file mode 100755
index 000000000..2315cc233
--- /dev/null
+++ b/intTests/test0220/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw