diff -durN pvs-4.2.ORIG/ess/dist-ess.lisp pvs-4.2/ess/dist-ess.lisp
--- pvs-4.2.ORIG/ess/dist-ess.lisp	2010-01-28 14:02:29.253087714 -0700
+++ pvs-4.2/ess/dist-ess.lisp	2010-01-28 13:56:38.670112938 -0700
@@ -112,8 +112,8 @@
 
 (defun save-ess-lisp (ess-filename features)
   (let ((feature-alist (filter-features features)))
-    (let ((ess-string (format nil #-GCL "~{~A~:^, ~}."
-			          #+GCL "~{~A~^, ~}."
+    (let ((ess-string (format nil #-(or GCL sbcl) "~{~A~:^, ~}."
+			          #+(or GCL sbcl) "~{~A~^, ~}."
 			      (mapcar #'fourth feature-alist))))
       (format t "Now disksaving ... ")
       (let ((in-reborn-image-p nil)
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp pvs-4.2/ess/lang/sb-term/rel/access.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp	2010-01-28 14:02:29.253087714 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/access.lisp	2010-01-28 13:56:38.671110580 -0700
@@ -22,11 +22,16 @@
 
 ;;(in-package "SB" :nicknames '("SYNTAX-BOX"))
 
-(in-package :syntax-box :nicknames '(:sb)) (use-package :ergolisp)
-
-
-(use-package '(:oper :term :sort :sb-runtime :lang))
+#+sbcl
+(eval-when (:compile-toplevel :load-toplevel :execute)
+  (unless (find-package :syntax-box)
+    (defpackage :syntax-box (:nicknames "SB")
+      (:use :common-lisp :ergolisp :oper :term :sort :sb-runtime :lang)
+      (:shadowing-import-from :sb-int memq))))
+(in-package :syntax-box)
 
+#-sbcl (use-package :ergolisp)
+#-sbcl (use-package '(:oper :term :sort :sb-runtime :lang))
 
 (defparameter *sb-package* (find-package :sb))
 
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/sb-parser.lisp pvs-4.2/ess/lang/sb-term/rel/sb-parser.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/sb-parser.lisp	2010-01-28 14:02:29.254040118 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/sb-parser.lisp	2010-01-28 13:56:38.672110397 -0700
@@ -8,7 +8,7 @@
 
 (export '( sb-parse ))
 
-(defparameter sb-abs-syn-package (find-package "syntax-box")) 
+(defparameter sb-abs-syn-package (find-package :syntax-box)) 
 
 (defun sb-parse (&key (nt 'meta-grammar) error-threshold ask-about-bad-tokens
   (return-errors nil) (stream nil streamp) string file (exhaust-stream nil))
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/top.lisp pvs-4.2/ess/lang/sb-term/rel/top.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/top.lisp	2010-01-28 14:02:29.255082752 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/top.lisp	2010-01-28 13:56:38.673110286 -0700
@@ -29,9 +29,9 @@
 
 (export '(sb sb-make))
 
-(defconstant sb-version "1 Feb 88")
+(defconstant-if-unbound sb-version "1 Feb 88")
 
-(defconstant gen-src-file-ext "lisp")
+(defconstant-if-unbound gen-src-file-ext "lisp")
 
 
 (defmacro string-empty? (s)
diff -durN pvs-4.2.ORIG/Makefile.in pvs-4.2/Makefile.in
--- pvs-4.2.ORIG/Makefile.in	2010-01-28 14:02:29.256085875 -0700
+++ pvs-4.2/Makefile.in	2010-01-28 14:02:12.136086081 -0700
@@ -94,7 +94,7 @@
 
 ifneq ($(SBCLISP_HOME),)
 # Check that the given SBCLISP_HOME works
-SBCLISPEXE = $(SBCLISP_HOME)/run-sbcl.sh
+SBCLISPEXE = $(SBCLISP_HOME)/sbcl
 ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK)
 SBCLVERSION = $(shell $(SBCLISPEXE) --version)
 $(warning "$(SBCLVERSION)")
@@ -532,9 +532,7 @@
 		      --eval "(unwind-protect \
 				  (mk:operate-on-system :pvs :compile) \
 				(save-lisp-and-die \"$@\" \
-				    :toplevel (function startup-pvs) \
-                                    :executable t \
-			       ))"
+				    :toplevel (function startup-pvs)))"
 	-rm $(PVSPATH)BDD/$(PLATFORM)/bdd-sbcl.*
 	cp $(SBCLISPEXE) $(subst $(SYSTEM)-sbclisp,,$@)
 	cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@)
diff -durN pvs-4.2.ORIG/pvs.in pvs-4.2/pvs.in
--- pvs-4.2.ORIG/pvs.in	2010-01-28 14:02:29.257083071 -0700
+++ pvs-4.2/pvs.in	2010-01-28 14:02:12.136086081 -0700
@@ -261,9 +261,9 @@
         then PVSLISP=cmulisp
         elif [ -x $binpath/runtime/pvs-cmulisp ]
         then PVSLISP=cmulisp
-	elif [ -x $binpath/devel/pvs-sbclisp ]
+	elif [ -e $binpath/devel/pvs-sbclisp ]
 	then PVSLISP=sbclisp
-	elif [ -x $binpath/runtime/pvs-sbclisp ]
+	elif [ -e $binpath/runtime/pvs-sbclisp ]
 	then PVSLISP=sbclisp
         else echo "No executable available in $binpath"
              exit 1
@@ -271,11 +271,11 @@
 fi
 PVSIMAGE=pvs-$PVSLISP
 
-if [ -d $binpath/devel -a -x $binpath/devel/$PVSIMAGE -a ! "$pvsruntime" ]
+if [ -d $binpath/devel -a -e $binpath/devel/$PVSIMAGE -a ! "$pvsruntime" ]
    then PATH=$binpath/devel:$binpath:$PVSPATH/bin:$PATH
     LD_LIBRARY_PATH=$binpath/devel:$LD_LIBRARY_PATH
     DYLD_LIBRARY_PATH=$binpath/devel:$DYLD_LIBRARY_PATH
-elif [ -d $binpath/runtime -a -x $binpath/runtime/$PVSIMAGE ]
+elif [ -d $binpath/runtime -a -e $binpath/runtime/$PVSIMAGE ]
    then PATH=$binpath/runtime:$binpath:$PVSPATH/bin:$PATH
     LD_LIBRARY_PATH=$binpath/runtime:$LD_LIBRARY_PATH
     DYLD_LIBRARY_PATH=$binpath/runtime:$DYLD_LIBRARY_PATH
@@ -316,6 +316,11 @@
 	    for lf in $lisploadfiles
 	    do flags="$flags --load $lf"; done
 	fi
+	if [ -d $binpath/devel -a -e $binpath/devel/$PVSIMAGE ]; then
+	  PVSIMAGE="/usr/bin/sbcl --core $binpath/devel/$PVSIMAGE"
+	else
+	  PVSIMAGE="/usr/bin/sbcl --core $binpath/runtime/$PVSIMAGE"
+	fi
 	;;
 esac
 
diff -durN pvs-4.2.ORIG/src/defsystem.lisp pvs-4.2/src/defsystem.lisp
--- pvs-4.2.ORIG/src/defsystem.lisp	2010-01-28 14:02:29.259088978 -0700
+++ pvs-4.2/src/defsystem.lisp	2010-01-28 13:56:38.677110470 -0700
@@ -1783,6 +1783,10 @@
 	(push :case-sensitive common-lisp:*features*)
       (push :case-insensitive common-lisp:*features*))))
 
+#+sbcl
+(eval-when (:compile-toplevel :load-toplevel :execute)
+  (push #+:unix :case-sensitive #-:unix :case-insensitive
+	common-lisp:*features*))
 
 #+(and allegro case-sensitive ics)
 (compiler-type-translation "excl 6.1" "excl-m")
diff -durN pvs-4.2.ORIG/src/globals.lisp pvs-4.2/src/globals.lisp
--- pvs-4.2.ORIG/src/globals.lisp	2010-01-28 14:02:29.259932686 -0700
+++ pvs-4.2/src/globals.lisp	2010-01-28 13:56:38.678129507 -0700
@@ -293,7 +293,7 @@
 
 ;; Used to keep track of which expression have already gone through
 ;; check-type-actuals processing
-(defvar *exprs-generating-actual-tccs*)
+(defvar *exprs-generating-actual-tccs* nil)
 
 ;;; Associate old tcc names with new tccs, so that proofs may be restored.
 (defvar *old-tcc-names* nil)
diff -durN pvs-4.2.ORIG/src/list-decls.lisp pvs-4.2/src/list-decls.lisp
--- pvs-4.2.ORIG/src/list-decls.lisp	2010-01-28 14:02:29.262087873 -0700
+++ pvs-4.2/src/list-decls.lisp	2010-01-28 13:56:38.679110647 -0700
@@ -103,7 +103,7 @@
       (pvs-message "~a has not been typechecked" oname)))
 
 (defun typechecked-origin? (name origin)
-  (case (intern (string-downcase origin))
+  (case (intern (#+allegro string-downcase #-allegro string-upcase origin))
     ((ppe tccs) (get-theory name))
     ((prelude prelude-theory) t)
     (t (typechecked-file? name))))
@@ -301,7 +301,7 @@
     (values object containing-type)))
 
 (defun get-syntactic-objects-for (name origin)
-  (case (intern (string-downcase origin))
+  (case (intern (#+allegro string-downcase #-allegro string-upcase origin))
     (ppe (let ((theory (get-theory name)))
 	   (when theory
 	     (values (ppe-form theory) (list theory)))))
diff -durN pvs-4.2.ORIG/src/parse.lisp pvs-4.2/src/parse.lisp
--- pvs-4.2.ORIG/src/parse.lisp	2010-01-05 02:06:15.000000000 -0700
+++ pvs-4.2/src/parse.lisp	2010-01-28 14:09:48.799985842 -0700
@@ -1129,12 +1129,12 @@
   (let ((pos? (is-sop 'POS (term-arg0 rat-term)))
 	(num (ds-number (term-arg1 rat-term))))
     (when (zerop num)
-      (parse-error ))
+      (parse-error 0 "Ratio with 0 numerator is just 0"))
     (if (is-sop 'NODEN (term-arg2 rat-term))
 	(if pos? num (- num))
 	(let ((den (ds-number (term-arg2 rat-term))))
 	  (when (zerop den)
-	    (parse-error ))
+	    (parse-error 0 "Cannot have a ratio with 0 denominator"))
 	  (if pos? (/ num den) (- (/ num den)))))))
 
 (defun xt-var-decl (var-decl)
diff -durN pvs-4.2.ORIG/src/pvs.lisp pvs-4.2/src/pvs.lisp
--- pvs-4.2.ORIG/src/pvs.lisp	2010-01-28 14:02:29.263960488 -0700
+++ pvs-4.2/src/pvs.lisp	2010-01-28 13:56:38.681109867 -0700
@@ -2143,7 +2143,9 @@
 	  (unproved? (pvs-message "No more unproved formulas below"))
 	  (t (pvs-message
 		 "Not at a formula declaration~@[ - ~a buffer may be invalid~]"
-	       (car (member (intern (string-downcase origin)) '(tccs ppe))))))))
+	       (car (member (intern #+allegro (string-downcase origin)
+				    #-allegro (string-upcase origin))
+			    '(tccs ppe))))))))
 
 (defun prove-formula (theoryname formname rerun?)
   (let ((theory (get-typechecked-theory theoryname)))
@@ -3265,7 +3267,8 @@
   
 
 (defun show-strategy (strat-name)
-  (let* ((strat-id (intern (string-downcase strat-name)))
+  (let* ((strat-id (intern #+allegro (string-downcase strat-name)
+			   #-allegro (string-upcase strat-name)))
 	 (strategy (or (gethash strat-id *rulebase*)
 		       (gethash strat-id *steps*)
 		       (gethash strat-id *rules*))))
diff -durN pvs-4.2.ORIG/src/rahd/cocoa.lisp pvs-4.2/src/rahd/cocoa.lisp
--- pvs-4.2.ORIG/src/rahd/cocoa.lisp	2010-01-28 14:02:29.264966823 -0700
+++ pvs-4.2/src/rahd/cocoa.lisp	2010-01-28 14:16:56.317109669 -0700
@@ -56,7 +56,8 @@
 			      (format cocoa-gb-in cocoa-gb-str))
 	      (#+allegro excl:run-shell-command
 			 #+cmu extensions:run-program
-			 "./cocoa-gb.bash")
+			 #+sbcl sb-ext:run-program
+			 "./cocoa-gb.bash" #+sbcl nil)
 	      (let ((computed-gbasis-lst nil))
 		(with-open-file (cocoa-gb-out (work-pathify "cocoa-gb.out") :direction :input)
 		   (do ((l (read-line cocoa-gb-out) (read-line cocoa-gb-out nil 'eof)))
diff -durN pvs-4.2.ORIG/src/rahd/opencad.lisp pvs-4.2/src/rahd/opencad.lisp
--- pvs-4.2.ORIG/src/rahd/opencad.lisp	2010-01-28 14:02:29.264966823 -0700
+++ pvs-4.2/src/rahd/opencad.lisp	2010-01-28 14:16:30.164986452 -0700
@@ -57,10 +57,11 @@
 	     (let ((error-code
 		    (#+allegro excl:run-shell-command
 			       #+cmu extensions:run-program
-			       "qepcad.bash")))
+			       #+sbcl sb-ext:run-program
+			       "qepcad.bash" #+sbcl nil)))
 	       (fmt 10 "~% [CAD] :: Sys-call for QEPCAD.BASH successfull with exit code: ~A. ~%" error-code)
 	       (if #+allegro (= error-code 0)
-		 #+cmu t ;; Need to learn how to get CMUCL error code here.
+		 #-allegro t ;; Need to learn how to get CMUCL error code here.
 		 (with-open-file (cad-output "proofobl.out" :direction :input)
 				 (let ((cad-decision (read-line cad-output nil)))
 				   (fmt 10 "~% [CAD] :: CAD decision: ~A ;  Generic? ~A. ~%" cad-decision generic)
diff -durN pvs-4.2.ORIG/src/rahd/rahd.lisp pvs-4.2/src/rahd/rahd.lisp
--- pvs-4.2.ORIG/src/rahd/rahd.lisp	2010-01-28 14:02:29.265965379 -0700
+++ pvs-4.2/src/rahd/rahd.lisp	2010-01-28 14:19:29.177984615 -0700
@@ -66,6 +66,9 @@
 (defun compile-file-and-load (&rest fnames)
   (mapcar #'(lambda (fname) 
 	      (let ((fname-full (format nil "~D.lisp" fname)))
+		#+sbcl
+		(load (compile-file fname-full :verbose t))
+		#-sbcl
 		(compile-file fname-full :load-after-compile t :verbose t)
 		(format t "~%[RAHD-REBOOT]: ~D compiled and loaded successfully." fname-full)))
 	      fnames))
@@ -132,8 +135,7 @@
 			    build-name))
     (fmt 0 "..... DONE.~%")
     (fmt 0 "          Marking executable +x .......")
-    (#+allegro excl:run-shell-command #+cmu extensions:run-program
-	       (format nil "chmod +x ~A.exec" build-name))
+    (pvs::chmod "+x" (format nil "~A.exec" build-name))
     (fmt 0 "..... DONE.~%~% >> [RAHD-BUILD-STAND-ALONE]: Process complete.~%"))
   t)
 
diff -durN pvs-4.2.ORIG/src/status-cmds.lisp pvs-4.2/src/status-cmds.lisp
--- pvs-4.2.ORIG/src/status-cmds.lisp	2010-01-28 14:02:29.266965505 -0700
+++ pvs-4.2/src/status-cmds.lisp	2010-01-28 13:56:38.685115340 -0700
@@ -1007,7 +1007,7 @@
   (if (and (member origin '("ppe" "tccs") :test #'string=)
 	   (not (get-theory bufname)))
       (pvs-message "~a is not typechecked" bufname)
-      (case (intern (string-downcase origin))
+      (case (intern (#+allegro string-downcase #-allegro string-upcase origin))
 	(ppe (let* ((theories (ppe-form (get-theory bufname)))
 		    (decl (get-decl-at line t theories)))
 	       (values (find-if #'(lambda (d) (and (declaration? d)
diff -durN pvs-4.2.ORIG/src/utils.lisp pvs-4.2/src/utils.lisp
--- pvs-4.2.ORIG/src/utils.lisp	2010-01-28 14:02:29.267928254 -0700
+++ pvs-4.2/src/utils.lisp	2010-01-28 13:56:38.686110351 -0700
@@ -324,7 +324,7 @@
 
 #+sbcl
 (defun working-directory ()
-  (pathname (sb-posix:getcwd)))
+  (make-pathname :directory (sb-posix:getcwd)))
 
 #+sbcl
 (defun set-working-directory (dir)
diff -durN pvs-4.2.ORIG/src/WS1S/lisp/dfa-foreign-sbcl.lisp pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp
--- pvs-4.2.ORIG/src/WS1S/lisp/dfa-foreign-sbcl.lisp	1969-12-31 17:00:00.000000000 -0700
+++ pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp	2010-01-28 13:56:38.687110660 -0700
@@ -0,0 +1,275 @@
+;; --------------------------------------------------------------------
+;; PVS
+;; Copyright (C) 2006, SRI International.  All Rights Reserved.
+
+;; This program is free software; you can redistribute it and/or
+;; modify it under the terms of the GNU General Public License
+;; as published by the Free Software Foundation; either version 2
+;; of the License, or (at your option) any later version.
+
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program; if not, write to the Free Software
+;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+;; --------------------------------------------------------------------
+
+(in-package :pvs)
+
+;; Structure of a DFA in foreign space
+(sb-alien:define-alien-type nil
+  (sb-alien:struct mona-dfa
+   (bddm (* t))              ; Manager of BDD nodes
+   (ns   (integer 32))       ; Number of states
+   (q    (* t))              ; Transition array
+   (s    (integer 32))       ; Start State
+   (f    (* (integer 32))))) ; State Status Array
+
+;; Predefined basic automata
+
+(sb-alien:define-alien-routine ("ws1s___dfaTrue" mona-true)     ; true
+  (* (sb-alien:struct mona-dfa)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaFalse" mona-false)   ; false
+  (* (sb-alien:struct mona-dfa)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaConst" mona-const)   ; p_i = n
+  (* (sb-alien:struct mona-dfa))
+  (n (integer 32)) (i (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaLess" mona-less)     ; p_i < p_j
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaLesseq" mona-lesseq) ; p_i <= p_j
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPlus1" mona-plus1)   ;  p_i = p_j + n
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)) (n (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinus1" mona-minus1) ;  p_i = p_i - p_j
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaEq1" mona-eq1)       ; p_i = p_j
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaEq2" mona-eq2)       ; P_i = P_j
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPlus2" mona-plus2)   ; P_i = P_j + 1
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinus2" mona-minus2) ; P_i = P_j - 1
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPlusModulo1" mona-plusmodulo1) ;  p_i = p_j + 1 % p_k
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinusModulo1" mona-minusmodulo1) ;  p_i = p_j - 1 % p_k
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaEmpty" mona-empty)   ; P_i = empty
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaIn" mona-in) ; p_i in P_j  recognizes <X,X>(<0,X>+)<1,1>(<X,X>*)
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaSubset" mona-subset) ; P_i sub P_j
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaUnion" mona-union)   ; P_i = P_j union P_k
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaInter" mona-intersection) ; P_i = P_j inter P_k
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaSetminus" mona-difference) ; P_i = P_j \ P_k
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMax" mona-max)       ;  p_i = max(P_j)
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMin" mona-min)       ;  p_i = min(P_j)
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaBoolvar" mona-boolvar) ; b_i
+  (* (sb-alien:struct mona-dfa))
+  (b (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPresbConst" mona-presburger-const) ; P_i = pconst(n)
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)) (n (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaSingleton" mona-singleton) ; singleton(P_i)
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaFirstOrder" mona-first-order) ; recognizes 0*1+
+  (* (sb-alien:struct mona-dfa))
+  (i (integer 32)))
+
+
+;; Automaton operations
+
+(sb-alien:define-alien-routine ("ws1s___dfaFree" mona-free!)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaNegation" mona-negation!)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaRestrict" mona-restrict!)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaUnrestrict" mona-unrestrict!)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaCopy" mona-copy)
+  (* (sb-alien:struct mona-dfa))
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaProduct" mona-product)
+  (* (sb-alien:struct mona-dfa))
+  (a1 (* (sb-alien:struct mona-dfa)))
+  (a2 (* (sb-alien:struct mona-dfa)))
+  (mode (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrefixClose" mona-prefix-close!)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaConjunction" mona-conjunction)
+  (* (sb-alien:struct mona-dfa))
+  (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaDisjunction" mona-disjunction)
+  (* (sb-alien:struct mona-dfa))
+  (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaImplication" mona-implication)
+  (* (sb-alien:struct mona-dfa))
+  (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaIff" mona-iff)
+  (* (sb-alien:struct mona-dfa))
+  (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaStatus" mona-status)
+  (integer 32)
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaProject" mona-project)
+				; projects away track var_index from a and
+				; determinizes the resulting automaton
+  (* (sb-alien:struct mona-dfa))
+  (a (* (sb-alien:struct mona-dfa))) (index (sb-alien:unsigned 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaRightQuotient" mona-right-quotient!)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))) (index (sb-alien:unsigned 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinimize" mona-minimize) ; Minimization
+  (* (sb-alien:struct mona-dfa))
+  (a (* (sb-alien:struct mona-dfa))))
+
+
+;; Analysis and printing
+
+(sb-alien:define-alien-routine ("ws1s___dfaMakeExample" mona-make-example)
+  sb-alien:c-string
+  (a (* (sb-alien:struct mona-dfa)))
+  (kind (integer 32))
+  (num (integer 32))
+  (indices (array (sb-alien:unsigned 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaAnalyze" mona-analyze)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa)))
+  (num (integer 32))
+  (names (array sb-alien:c-string))
+  (indices (array sb-alien:unsigned))
+  (orders (array sb-alien:char))
+  (treestyle (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrintVitals" mona-print-vitals)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrint" mona-print)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa)))
+  (num (integer 32))
+  (names (array sb-alien:c-string))
+  (indices (array (sb-alien:unsigned 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrintGraphviz" mona-print-graphviz)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa)))
+  (num (integer 32))
+  (indices (array (sb-alien:unsigned 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrintVerbose" mona-print-verbose)
+  sb-alien:void
+  (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___bdd_size" bdd-size)
+  (sb-alien:unsigned 32)
+  (bbdm (* t)))
+
+
+;; Constructing Automata Explicitly
+
+(sb-alien:define-alien-routine ("ws1s___dfaSetup" mona-setup)
+  sb-alien:void
+  (s (integer 32))
+  (len (integer 32))
+  (indices (array (integer 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaAllocExceptions" mona-alloc-exceptions)
+  sb-alien:void
+  (n (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaStoreException" mona-store-exception)
+  sb-alien:void
+  (s (integer 32)) (path sb-alien:c-string))
+
+(sb-alien:define-alien-routine ("ws1s___dfaStoreState" mona-store-state)
+  sb-alien:void
+  (s (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaBuild" mona-build)
+  (* (sb-alien:struct mona-dfa))
+  (statuses (array sb-alien:char)))
+
+;; Exporting
+
+(sb-alien:define-alien-routine ("ws1s___dfaExport" mona-export)
+  (integer 32)
+  (a (* (sb-alien:struct mona-dfa)))
+  (filename sb-alien:c-string)
+  (num (integer 32))
+  (names (array sb-alien:c-string))
+  (orders (array sb-alien:char)))