--- a/bin/pvs-platform.orig	2020-01-23 00:17:15.000000000 -0700
+++ b/bin/pvs-platform	2020-01-27 11:10:12.334492312 -0700
@@ -33,10 +33,7 @@ case `uname -s` in
 	 esac
 	 os=SunOS
          os_version=`uname -r | cut -d"." -f1`;;
-  Linux|FreeBSD) case `uname -m` in
-	   x86_64) arch=ix86_64;;
-	   *86*)   arch=ix86;;
-	 esac
+  Linux|FreeBSD)   arch=linux
 	 os=Linux;;
   AIX) arch=powerpc-ibm
        os=AIX
--- a/Makefile.in.orig	2020-01-23 00:17:15.000000000 -0700
+++ b/Makefile.in	2020-01-27 11:10:12.374491828 -0700
@@ -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.orig	2020-01-23 00:17:15.000000000 -0700
+++ b/pvs-config.lisp	2020-01-27 11:19:14.701917754 -0700
@@ -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*))))
 
@@ -85,8 +86,8 @@
   #+(and cmu linux) "x86f"
   #+(and cmu darwin) "ppcf"
   #+(and cmu solaris) "sparcf"
-  #+(and sbcl x86-64 linux) "fasl"
-  #+(and sbcl (not x86-64) linux) "x86s"
+  #+(and sbcl linux x86 (not x86-64)) "x86s"
+  #+(and sbcl linux (or (not x86) x86-64)) "fasl"
   #+(and sbcl darwin) "ppcs"
   #+(and sbcl sparc) "sparcs"
   #+(and clisp pc386) "clfasl"
--- a/pvs.in.orig	2020-01-23 00:17:15.000000000 -0700
+++ b/pvs.in	2020-01-27 11:10:12.374491828 -0700
@@ -233,15 +233,8 @@ case $opsys in
 	 case `uname -m` in
 	   x86_64) PVSARCH=ix86_64 ;;
 	   *86*)   PVSARCH=ix86 ;;
-	   *) echo "PVS only runs on Intel under Linux"; exit 1
+	   *)      PVSARCH=$(uname -m) ;;
 	 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=
@@ -276,11 +269,7 @@ case $opsys in
   *) echo "PVS only runs under Solaris, Linux, FreeBSD (linux-enabled), or MacOSX"; exit 1
 esac
 
-PVSBINPATH=$PVSPATH/bin/$PVSARCH-$opsys${majvers}
-# Check if this is a 64-bit platform, but only 32-bit available
-if [ "$PVSARCH" = "ix86_64" -a ! -x "$PVSBINPATH" ]
-    then PVSBINPATH=$PVSPATH/bin/ix86-$opsys${majvers}
-fi
+PVSBINPATH=$PVSPATH/bin/linux-Linux
 
 if [ -n "$PVSLISP" -a "$PVSLISP" != "allegro" -a "$PVSLISP" != "cmulisp" -a "$PVSLISP" != "sbclisp" ]
   then echo "ERROR: PVSLISP must be unset, or set to 'allegro', 'cmulisp', or 'sbclisp'"
--- a/src/BDD/linux-Linux/Makefile.orig	2020-01-27 11:10:12.375491816 -0700
+++ b/src/BDD/linux-Linux/Makefile	2020-01-27 11:10:12.375491816 -0700
@@ -0,0 +1,49 @@
+BDD = ../bdd/src
+MU = ../mu/src
+UTILS = ../bdd/utils
+INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU)
+#LD = gcc
+#LDFLAGS = -shared -L./
+LD = gcc
+LDFLAGS = -Xlinker -Bsymbolic -shared -L./ @LDFLAGS@
+CC = gcc
+CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC @CFLAGS@
+XCFLAGS = -O
+SHELL = /bin/sh
+VPATH = ..:../bdd/utils:../bdd/src:../mu/src
+
+muobj = bdd_interface.o bdd.o bdd_factor.o bdd_quant.o bdd_fns.o bdd_vfns.o \
+        appl.o mu_interface.o mu.o
+
+utilobj = double.o list.o hash.o alloc.o
+
+.SUFFIXES:
+.SUFFIXES: .c .o
+.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
+
+all : mu.so
+
+mu.so : ${muobj} libutils.a ../bdd-ld-table ../mu-ld-table 
+	$(CC) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm
+
+libutils.a : ${utilobj}
+	ar r libutils.a ${utilobj}
+	ranlib libutils.a
+
+bdd_interface.o : bdd_interface.c bdd_fns.h
+bdd_factor.o : bdd_factor.c bdd_factor.h
+bdd.o : bdd.c bdd.h bdd_extern.h
+bdd_fns.o : bdd_fns.c bdd_fns.h bdd.h bdd_extern.h
+bdd_quant.o : bdd_quant.c bdd_fns.h bdd.h bdd_extern.h
+bdd_vfns.o : bdd_vfns.c bdd_vfns.h bdd_fns.h bdd.h bdd_extern.h
+
+mu_interface.o : mu_interface.c mu.h
+mu.o : mu.c mu.h
+
+double.o : double.c double.h
+list.o : list.c list.h alloc.h
+hash.o : hash.c hash.h alloc.h
+alloc.o : alloc.c
+
+clean : 
+	rm -f *.o *.a *.so
--- a/src/classes-expr.lisp.orig	2020-01-23 00:17:15.000000000 -0700
+++ b/src/classes-expr.lisp	2020-01-27 11:10:12.375491816 -0700
@@ -34,8 +34,9 @@
 	  equation iff iff-or-boolean-equation implication index negation
 	  propositional-application))
 
-;; SBCL changed things so this no longer works - pvs.system
-;; simply unlocks the :common-lisp package
+#+sbcl
+(eval-when (:execute :compile-toplevel :load-toplevel)
+  (sb-ext:unlock-package :common-lisp))
 #+cmu
 (ext:without-package-locks
  (defgeneric type (x))
--- a/src/utils/linux-Linux/Makefile.orig	2020-01-27 11:10:12.376491804 -0700
+++ b/src/utils/linux-Linux/Makefile	2020-01-27 11:10:12.376491804 -0700
@@ -0,0 +1,23 @@
+LD = gcc
+LDFLAGS = -shared -L./ @LDFLAGS@
+CC=gcc
+CFLAGS=-fPIC @CFLAGS@
+WFLAGS=-Wall
+VPATH=..
+
+obj=file_utils.o
+
+.SUFFIXES:
+.SUFFIXES: .c .o
+.c.o : ; $(CC) $(XCFLAGS) ${WFLAGS} ${CFLAGS} -c $< -o $@
+
+all : file_utils.so b64
+
+file_utils.so: ${obj}
+	$(LD) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj} -lc
+
+b64: ../b64.c
+	$(CC) -o ./b64 ../b64.c
+
+clean :
+	rm -f *.o *.a *.so b64
--- a/src/WS1S/linux-Linux/Makefile.orig	2020-01-27 11:10:12.379491768 -0700
+++ b/src/WS1S/linux-Linux/Makefile	2020-01-27 11:10:12.379491768 -0700
@@ -0,0 +1,67 @@
+ifneq (,)
+This makefile requires GNU Make.
+endif
+
+BDD = ../mona/BDD
+DFA = ../mona/DFA
+UTILS = ../mona/Mem
+INCLUDES = -I$(BDD) -I$(DFA) -I$(UTILS)
+LD = gcc
+LDFLAGS = -shared -L./ @LDFLAGS@
+CC = gcc
+CFLAGS += -fPIC -D_POSIX_SOURCE -DSYSV -D_BSD_SOURCE $(INCLUDES) @CFLAGS@
+XCFLAGS = -O
+SHELL = /bin/sh
+VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
+
+#obj  = ws1s_table.o ws1s_extended_interface.o -lmonadfa
+
+obj  = analyze.o prefix.o product.o \
+       quotient.o basic.o external.o \
+       makebasic.o minimize.o printdfa.o \
+       project.o dfa.o \
+       bdd.o bdd_double.o bdd_external.o \
+       bdd_manager.o hash.o bdd_dump.o \
+       bdd_trace.o bdd_cache.o \
+       dlmalloc.o mem.o \
+       ws1s_table.o \
+       ws1s_extended_interface.o
+
+.SUFFIXES:
+.SUFFIXES: .c .o
+.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
+
+all : ws1s.so
+
+ws1s_extended_interface.o : ../ws1s_extended_interface.c
+	$(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
+
+ws1s.so : ${obj}
+	$(CC) -shared $(CFLAGS) -o ws1s.so ${obj} $(LDFLAGS) -lmonabdd
+
+bdd.o: bdd.c bdd.h bdd_internal.h
+bdd_double.o: bdd_double.c bdd.h bdd_internal.h
+bdd_external.o: bdd_external.c bdd_external.h mem.h
+bdd_manager.o: bdd_manager.c bdd.h bdd_internal.h
+hash.o: hash.c mem.h hash.h
+bdd_dump.o: bdd_dump.c bdd_dump.h
+bdd_trace.o: bdd_trace.c bdd.h bdd_internal.h
+bdd_cache.o: bdd_cache.c bdd.h bdd_internal.h
+
+analyze.o: analyze.c dfa.h mem.h
+prefix.o: prefix.c dfa.h mem.h
+product.o: product.c dfa.h bdd.h hash.h mem.h
+quotient.o: quotient.c dfa.h hash.h mem.h
+basic.o: basic.c dfa.h mem.h
+external.o: external.c dfa.h bdd_external.h mem.h
+makebasic.o: makebasic.c dfa.h bdd_internal.h
+minimize.o: minimize.c dfa.h hash.h mem.h
+printdfa.o: printdfa.c dfa.h mem.h
+project.o: project.c dfa.h hash.h mem.h
+dfa.o: dfa.c dfa.h bdd.h hash.h mem.h
+
+dlmalloc.o: dlmalloc.c dlmalloc.h
+mem.o: mem.c dlmalloc.h
+
+clean : 
+	rm -f *.o *.a *.so
--- a/src/WS1S/ws1s-ld-table.orig	2020-01-23 00:17:15.000000000 -0700
+++ b/src/WS1S/ws1s-ld-table	2020-01-27 11:10:12.379491768 -0700
@@ -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.orig	2020-01-23 00:17:15.000000000 -0700
+++ b/src/WS1S/ws1s_table.c	2020-01-27 11:10:12.379491768 -0700
@@ -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);