diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
index 3c3e2e12e..2319bbb42 100755
--- a/test/coq/run_tests.sh
+++ b/test/coq/run_tests.sh
@@ -47,7 +47,7 @@ function check_tests_dir {
     TESTSDIR="$1"
     for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`;
     do
-        if $SAIL -coq -coq-lib-style stdpp -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null;
+        if $SAIL -coq -coq-lib-style stdpp -dcoq_undef_axioms --strict-bitvector -o out $TESTSDIR/$i &>/dev/null;
         then
     	if coqc $COQOPTS out_types.v &>/dev/null &&
     	   coqc $COQOPTS out.v &>/dev/null;
diff --git a/test/coq/skip b/test/coq/skip
index eac283ee4..bb856ea1d 100644
--- a/test/coq/skip
+++ b/test/coq/skip
@@ -51,6 +51,7 @@ XXXXX Need to be built against stdpp version of Sail (for now)
 concurrency_interface_dec.sail
 concurrency_interface_inc.sail
 XXXXX Would need to turn a term with existential type into a dependent pair
+ex_cons_infer.sail
 ex_list_infer.sail
 ex_vector_infer.sail
 XXXXX Would need float types in coq-sail