--- a/Makefile.in
+++ b/Makefile.in
@@ -169,7 +169,7 @@ endif
 
 ifneq ($(SBCLISP_HOME),)
 # Check that the given SBCLISP_HOME works
-SBCLISPEXE = $(SBCLISP_HOME)/run-sbcl.sh
+SBCLISPEXE = ./sbcl
 ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK)
 SBCLVERSION = $(shell $(SBCLISPEXE) --version)
 # $(warning "$(SBCLVERSION)")
--- a/pvs-config.lisp
+++ b/pvs-config.lisp
@@ -46,6 +46,7 @@
   (or #+allegro (sys:getenv "PVSPATH")
       #+gcl (si:getenv "PVSPATH")
       #+cmu (cdr (assoc :PVSPATH extensions::*environment-list*))
+      #+sbcl (sb-ext:posix-getenv "PVSPATH")
       ;; Assume this is loaded while cd'd to the PVS directory 
       (namestring (truename *default-pathname-defaults*))))
 
--- a/pvs.in
+++ b/pvs.in
@@ -235,13 +235,6 @@ case $opsys in
 	   *86*)   PVSARCH=ix86 ;;
 	   *) echo "PVS only runs on Intel under Linux"; exit 1
 	 esac
-	 # Allegro does not work with Linux's New Posix Thread Library (NPTL)
-	 # used in newer Red Hat kernels and 2.6 kernels.  This will force
-	 # the old thread-implementation.
-	 export LD_ASSUME_KERNEL=2.4.19;
-	 # See if setting this leads to problems - if it does, then
-	 # uname exits with an error and we unset it.
-	 uname -a > /dev/null 2>&1 || unset LD_ASSUME_KERNEL
 	 ;;
   FreeBSD) opsys=Linux
 	   majvers=
--- a/pvs.system
+++ b/pvs.system
@@ -160,7 +160,8 @@
 
 #+sbcl
 (eval-when (:execute :compile-toplevel :load-toplevel)
-  (sb-ext:unlock-package :common-lisp))
+  (sb-ext:unlock-package :common-lisp)
+  (sb-ext:unlock-package :sb-impl))
 
 #+cmu
 (eval-when (:execute :compile-toplevel :load-toplevel)
--- a/src/utils/ix86-Linux/Makefile
+++ b/src/utils/ix86-Linux/Makefile
@@ -1,4 +1,4 @@
-LD = ld
+LD = gcc
 LDFLAGS = -shared -L./
 CC=gcc
 CFLAGS=-fPIC
@@ -14,7 +14,7 @@ obj=file_utils.o
 all : file_utils.so b64
 
 file_utils.so: ${obj}
-	$(LD) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj} -lc
+	$(LD) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj}
 
 b64: ../b64.c
 	$(CC) -o ./b64 ../b64.c
--- a/src/WS1S/ix86_64-Linux/Makefile
+++ b/src/WS1S/ix86_64-Linux/Makefile
@@ -37,7 +37,7 @@ ws1s_extended_interface.o : ../ws1s_exte
 	$(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
 
 ws1s.so : ${obj}
-	$(CC) -shared $(CFLAGS) -o ws1s.so ${obj}
+	$(CC) -shared $(CFLAGS) -o ws1s.so ${obj} -lmonabdd
 
 bdd.o: bdd.c bdd.h bdd_internal.h
 bdd_double.o: bdd_double.c bdd.h bdd_internal.h
--- a/src/WS1S/ix86-Linux/Makefile
+++ b/src/WS1S/ix86-Linux/Makefile
@@ -36,7 +36,7 @@ ws1s_extended_interface.o : ../ws1s_exte
 	$(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
 
 ws1s.so : ${obj}
-	$(CC) -shared $(CFLAGS) -o ws1s.so ${obj}
+	$(CC) -shared $(CFLAGS) -o ws1s.so ${obj} -lmonabdd
 
 bdd.o: bdd.c bdd.h bdd_internal.h
 bdd_double.o: bdd_double.c bdd.h bdd_internal.h
--- a/src/WS1S/ws1s-ld-table
+++ b/src/WS1S/ws1s-ld-table
@@ -46,7 +46,7 @@ ws1s___dfaPrintVitals = dfaPrintVitals ;
 ws1s___dfaPrint = dfaPrint ;
 ws1s___dfaPrintGraphviz = dfaPrintGraphviz ;
 ws1s___dfaPrintVerbose = dfaPrintVerbose ;
-ws1s___bdd_size = mona_bdd_size ;
+ws1s___bdd_size = bdd_size ;
 ws1s___dfaSetup = dfaSetup ;
 ws1s___dfaAllocExceptions = dfaAllocExceptions ;
 ws1s___dfaStoreException = dfaStoreException ;
--- a/src/WS1S/ws1s_table.c
+++ b/src/WS1S/ws1s_table.c
@@ -182,8 +182,8 @@ extern int dfaPrintVerbose (int);
 int (*ws1s___dfaPrintVerbose)(int) = dfaPrintVerbose;
 
 
-extern int mona_bdd_size (int);
-int (*ws1s___bdd_size)(int) = mona_bdd_size;
+extern int bdd_size (int);
+int (*ws1s___bdd_size)(int) = bdd_size;
 
 
 extern int dfaSetup (int);