diff --git a/.scripts/test_package.sh b/.scripts/test_package.sh
index 85ac29748e8..0e589df628f 100755
--- a/.scripts/test_package.sh
+++ b/.scripts/test_package.sh
@@ -78,7 +78,7 @@ diag "-- Verify all examples --"
 if [[ -z "$CI_THREADS" ]] ; then
     CI_THREADS=1
 fi
-make -j "$CI_THREADS" -C /tmp/fstar_examples && make -j "$CI_THREADS" -C /tmp/fstar_doc/tutorial regressions
+make -j "$CI_THREADS" -C /tmp/fstar_examples HAS_OCAML= && make -j "$CI_THREADS" -C /tmp/fstar_doc/tutorial HAS_OCAMLFIND= regressions
 if [ $? -ne 0 ]; then
     echo -e "* ${RED}FAIL!${NC} for all examples - make returned $?"
     exit 1
diff --git a/examples/Makefile b/examples/Makefile
index ea61ad986eb..e81cfd107c1 100644
--- a/examples/Makefile
+++ b/examples/Makefile
@@ -20,15 +20,25 @@ all: prep verify special_cases
 
 EXCLUDE_DIRS=old/ hello/ native_tactics/ kv_parsing/ miniparse/ 
 
+# F* contrib directory needed by crypto/ . Since this Makefile
+# supersedes crypto/Makefile, we need to determine the location of the
+# F* contrib directory here.
+ifdef FSTAR_HOME
+FSTAR_UCONTRIB = $(shell if test -d $(FSTAR_HOME)/ucontrib ; then echo $(FSTAR_HOME)/ucontrib ; else echo $(FSTAR_HOME)/share/fstar/contrib ; fi)
+else
+   # FSTAR_HOME not defined, assume fstar.exe installed through opam
+   # or binary package, and reachable from PATH
+FSTAR_UCONTRIB=$(dir $(shell which fstar.exe))/../share/fstar/contrib
+endif
+
 INCLUDE_PATHS?= \
 	$(filter-out $(EXCLUDE_DIRS),$(shell ls -d */)) \
-	../ucontrib/CoreCrypto/fst \
-	../ucontrib/Platform/fst \
+	$(FSTAR_UCONTRIB)/CoreCrypto/fst \
+	$(FSTAR_UCONTRIB)/Platform/fst \
 	$(shell ls -d dsls/*/) \
 	$(shell ls -d verifythis/*/) \
-	$(shell ls -d demos/*/) \
 	tactics/eci19
-	
+
 include Makefile.common
 
 verify: prep $(filter-out $(CACHE_DIR)/Launch.fst.checked, $(ALL_CHECKED_FILES))
@@ -41,12 +51,12 @@ SPECIAL_CASES += native_tactics
 endif
 
 ifdef KRML_HOME
+SPECIAL_CASES += demos
 SPECIAL_CASES += kv_parsing
 SPECIAL_CASES += miniparse
 endif
 
 special_cases: $(addsuffix .all, $(SPECIAL_CASES))
-	$(MAKE) -C semiring CanonCommSemiring.native
 
 %.all: %
 	+$(MAKE) -C $^ all
diff --git a/tests/Makefile b/tests/Makefile
index 4521f962d1b..90b0531c3bb 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -10,6 +10,7 @@ ALL_TEST_DIRS += incl
 ALL_TEST_DIRS += machine_integers
 ALL_TEST_DIRS += micro-benchmarks
 ALL_TEST_DIRS += prettyprinting
+ALL_TEST_DIRS += semiring
 ALL_TEST_DIRS += struct
 ALL_TEST_DIRS += tactics
 ALL_TEST_DIRS += typeclasses
diff --git a/examples/semiring/CanonCommSemiring.Test.fst b/tests/semiring/CanonCommSemiring.Test.fst
similarity index 100%
rename from examples/semiring/CanonCommSemiring.Test.fst
rename to tests/semiring/CanonCommSemiring.Test.fst
diff --git a/examples/semiring/CanonCommSemiring.Test.fst.hints b/tests/semiring/CanonCommSemiring.Test.fst.hints
similarity index 100%
rename from examples/semiring/CanonCommSemiring.Test.fst.hints
rename to tests/semiring/CanonCommSemiring.Test.fst.hints
diff --git a/examples/semiring/CanonCommSemiring.fst b/tests/semiring/CanonCommSemiring.fst
similarity index 100%
rename from examples/semiring/CanonCommSemiring.fst
rename to tests/semiring/CanonCommSemiring.fst
diff --git a/examples/semiring/CanonCommSemiring.fst.hints b/tests/semiring/CanonCommSemiring.fst.hints
similarity index 100%
rename from examples/semiring/CanonCommSemiring.fst.hints
rename to tests/semiring/CanonCommSemiring.fst.hints
diff --git a/examples/semiring/CanonCommSemiring.ml.fixup b/tests/semiring/CanonCommSemiring.ml.fixup
similarity index 100%
rename from examples/semiring/CanonCommSemiring.ml.fixup
rename to tests/semiring/CanonCommSemiring.ml.fixup
diff --git a/examples/semiring/Makefile b/tests/semiring/Makefile
similarity index 100%
rename from examples/semiring/Makefile
rename to tests/semiring/Makefile