Add test case for #1788

The fix for #1828 also addresses many of the symptoms of #1788, so let's add
a test case to ensure that those symptoms remain cured.

intTests/test1788/Makefile

@@ -0,0 +1,17 @@
+CC = clang
+CFLAGS = -g -frecord-command-line -O0
+
+all: test.bc test.exe
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+test.o: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+test.exe: test.o
+	$(CC) $(CFLAGS) $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc test.exe

intTests/test1788/test.c

@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t mult(uint32_t x) {
+  return x * 0x85EBCA77U;
+}

intTests/test1788/test.saw

@@ -0,0 +1,13 @@
+// This test case ensures that ABC can prove that a C implementation of the
+// `mult` function is equivalent to a direct Cryptol implementation of the
+// same function.
+
+let
+{{
+cryptol_mult : [32] -> [32]
+cryptol_mult x = x * 0x85EBCA77
+}};
+
+m <- llvm_load_module "test.bc";
+llvm_mult <- llvm_extract m "mult";
+prove abc {{ \x -> llvm_mult x == cryptol_mult x }};

intTests/test1788/test.sh

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