diff --git a/.cvsignore b/.cvsignore
index e69de29..10067ef 100644
--- a/.cvsignore
+++ b/.cvsignore
@@ -0,0 +1 @@
+csisat-1.2.zip
diff --git a/csisat-makefile.patch b/csisat-makefile.patch
new file mode 100644
index 0000000..7044557
--- /dev/null
+++ b/csisat-makefile.patch
@@ -0,0 +1,191 @@
+diff -up ./Makefile.ORIG ./Makefile
+--- ./Makefile.ORIG	2008-07-08 22:38:05.000000000 -0600
++++ ./Makefile	2010-01-19 14:23:02.065649539 -0700
+@@ -65,8 +65,8 @@ TARGET = bin/csisat
+ OCAML_LIB = libcsisat
+ 
+ 
+-all: glpk pico picosat server $(FILES) $(MAIN) lib
+-	$(OCAML_OPT_C) $(COMPILE_FLAG) -o $(TARGET) $(LIBS)  $(GLPK) $(PWD)/picosat-632/libpicosat.a $(FILES) $(MAIN)
++all: glpk pico server $(FILES) $(MAIN) lib
++	$(OCAML_OPT_C) $(COMPILE_FLAG) -o $(TARGET) $(LIBS)  $(GLPK) $(FILES) $(MAIN)
+ 	$(shell sed -i 's/Version .*\\n\\n/Version 1.2 (Rev REV, Build DATE)\.\\n\\n/g' $(SRC)/csisatConfig.ml)
+ 
+ VERSION = $(shell svnversion)
+@@ -126,12 +126,12 @@ $(OBJ)/%.cmx: $(SRC)/%.ml
+ 
+ lib: $(LIB)/$(OCAML_LIB).cma $(LIB)/$(OCAML_LIB).cmxa 
+ 
+-$(LIB)/$(OCAML_LIB).cma: $(OCAML_LIB_OBJ:%=%.cmo)
++$(LIB)/$(OCAML_LIB).cma: $(OCAML_LIB_OBJ:%=%.cmo) $(FILES)
+ 	@echo Creating OCAML \(byte code\) library $@
+ 	@mkdir -p $(LIB)
+ 	$(OCAML_LD) $(OCAML_LD_FLAGS) -a -o $@ $(patsubst %.cmx, %.cmo, $(FILES))
+ 
+-$(LIB)/$(OCAML_LIB).cmxa $(LIB)/$(OCAML_LIB).a: $(OCAML_LIB_OBJ:%=%.cmx)
++$(LIB)/$(OCAML_LIB).cmxa $(LIB)/$(OCAML_LIB).a: $(OCAML_LIB_OBJ:%=%.cmx) $(FILES)
+ 	@echo Creating OCAML \(native code\) library $@
+ 	@mkdir -p $(LIB)
+ 	$(OCAML_OPT_LD) $(OCAML_LD_FLAGS) -a -o $@ $(FILES)
+@@ -155,26 +155,136 @@ odoc:
+ 		$(patsubst $(OBJ)/%, $(SRC)/%, $(patsubst %.cmx, %.ml, $(FILES)))
+ 
+ glpk:
+-	cd glpk_ml_wrapper; make
++	cd glpk_ml_wrapper; $(MAKE)
+ 	@mkdir -p $(LIB)
+ 	cp glpk_ml_wrapper/libcamlglpk.a $(LIB)/
+ 
+ pico:
+-	cd pico_ml_wrapper; make
++	cd pico_ml_wrapper; $(MAKE)
+ 	@mkdir -p $(LIB)
+ 	cp pico_ml_wrapper/libcamlpico.a $(LIB)/
+ 
+-picosat:
+-	cd picosat-632; ./configure;  make
+-	@mkdir -p $(LIB)
+-	cp picosat-632/libpicosat.a $(LIB)/
+-
+ server:
+-	cd server; make
++	cd server; $(MAKE)
+ 
+ clean:
+ 	$(RM) $(TARGET) $(OBJ)/* $(LIB)/*
+-	cd glpk_ml_wrapper; make clean
+-	cd pico_ml_wrapper; make clean
+-	cd picosat-632; make clean
+-	cd server; make clean
++	cd glpk_ml_wrapper; $(MAKE) clean
++	cd pico_ml_wrapper; $(MAKE) clean
++	cd server; $(MAKE) clean
++
++# Dependencies from ocamldep:
++$(OBJ)/csisatAstUtil.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \
++	$(OBJ)/csisatMessage.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatAstUtil.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \
++	$(OBJ)/csisatMessage.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatClpLI.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatMessage.cmo \
++	$(OBJ)/csisatMatrix.cmo $(OBJ)/csisatLIUtils.cmo \
++	$(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatClpLI.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatMessage.cmx \
++	$(OBJ)/csisatMatrix.cmx $(OBJ)/csisatLIUtils.cmx \
++	$(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatConfig.cmo: $(OBJ)/csisatSatPL.cmo $(OBJ)/csisatMessage.cmo \
++	$(OBJ)/csisatLIUtils.cmo
++$(OBJ)/csisatConfig.cmx: $(OBJ)/csisatSatPL.cmx $(OBJ)/csisatMessage.cmx \
++	$(OBJ)/csisatLIUtils.cmx
++$(OBJ)/csisatDag.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \
++	$(OBJ)/csisatMessage.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatDag.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \
++	$(OBJ)/csisatMessage.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatDpllClause.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatAstUtil.cmo \
++	$(OBJ)/csisatAst.cmo
++$(OBJ)/csisatDpllClause.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatAstUtil.cmx \
++	$(OBJ)/csisatAst.cmx
++$(OBJ)/csisatDpllCore.cmo: $(OBJ)/csisatSatInterface.cmo \
++	$(OBJ)/csisatOrdSet.cmo $(OBJ)/csisatMessage.cmo \
++	$(OBJ)/csisatDpllProof.cmo $(OBJ)/csisatDpllClause.cmo \
++	$(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatDpllCore.cmx: $(OBJ)/csisatSatInterface.cmx \
++	$(OBJ)/csisatOrdSet.cmx $(OBJ)/csisatMessage.cmx \
++	$(OBJ)/csisatDpllProof.cmx $(OBJ)/csisatDpllClause.cmx \
++	$(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatDpllProof.cmo: $(OBJ)/csisatDpllClause.cmo \
++	$(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatDpllProof.cmx: $(OBJ)/csisatDpllClause.cmx \
++	$(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatFociParse.cmo: $(OBJ)/csisatFociParse.cmi $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatFociParse.cmx: $(OBJ)/csisatFociParse.cmi $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatFociPrinter.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatFociPrinter.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatInfixParse.cmo: $(OBJ)/csisatInfixParse.cmi $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatInfixParse.cmx: $(OBJ)/csisatInfixParse.cmi $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatInterpolate.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatUIF.cmo \
++	$(OBJ)/csisatSatPL.cmo $(OBJ)/csisatSatLI.cmo $(OBJ)/csisatOrdSet.cmo \
++	$(OBJ)/csisatNelsonOppen.cmo $(OBJ)/csisatMessage.cmo \
++	$(OBJ)/csisatDpllProof.cmo $(OBJ)/csisatDag.cmo \
++	$(OBJ)/csisatClpLI.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatInterpolate.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatUIF.cmx \
++	$(OBJ)/csisatSatPL.cmx $(OBJ)/csisatSatLI.cmx $(OBJ)/csisatOrdSet.cmx \
++	$(OBJ)/csisatNelsonOppen.cmx $(OBJ)/csisatMessage.cmx \
++	$(OBJ)/csisatDpllProof.cmx $(OBJ)/csisatDag.cmx \
++	$(OBJ)/csisatClpLI.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatLIUtils.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \
++	$(OBJ)/csisatMessage.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatLIUtils.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \
++	$(OBJ)/csisatMessage.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatMain.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatPL.cmo \
++	$(OBJ)/csisatOrdSet.cmo $(OBJ)/csisatNelsonOppen.cmo \
++	$(OBJ)/csisatMessage.cmo $(OBJ)/csisatLIUtils.cmo \
++	$(OBJ)/csisatInterpolate.cmo $(OBJ)/csisatFociPrinter.cmo \
++	$(OBJ)/csisatConfig.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatMain.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatPL.cmx \
++	$(OBJ)/csisatOrdSet.cmx $(OBJ)/csisatNelsonOppen.cmx \
++	$(OBJ)/csisatMessage.cmx $(OBJ)/csisatLIUtils.cmx \
++	$(OBJ)/csisatInterpolate.cmx $(OBJ)/csisatFociPrinter.cmx \
++	$(OBJ)/csisatConfig.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatMatrix.cmo: $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatMatrix.cmx: $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatNelsonOppen.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatUIF.cmo \
++	$(OBJ)/csisatSatLI.cmo $(OBJ)/csisatOrdSet.cmo \
++	$(OBJ)/csisatMessage.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatNelsonOppen.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatUIF.cmx \
++	$(OBJ)/csisatSatLI.cmx $(OBJ)/csisatOrdSet.cmx \
++	$(OBJ)/csisatMessage.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatPicoInterface.cmo: $(OBJ)/csisatSatInterface.cmo \
++	$(OBJ)/csisatMessage.cmo $(OBJ)/csisatDpllProof.cmo \
++	$(OBJ)/csisatDpllClause.cmo $(OBJ)/csisatAstUtil.cmo \
++	$(OBJ)/csisatAst.cmo
++$(OBJ)/csisatPicoInterface.cmx: $(OBJ)/csisatSatInterface.cmx \
++	$(OBJ)/csisatMessage.cmx $(OBJ)/csisatDpllProof.cmx \
++	$(OBJ)/csisatDpllClause.cmx $(OBJ)/csisatAstUtil.cmx \
++	$(OBJ)/csisatAst.cmx
++$(OBJ)/csisatSatInterface.cmo: $(OBJ)/csisatDpllProof.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatSatInterface.cmx: $(OBJ)/csisatDpllProof.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatSatLI.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatMessage.cmo \
++	$(OBJ)/csisatMatrix.cmo $(OBJ)/csisatLIUtils.cmo \
++	$(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatSatLI.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatMessage.cmx \
++	$(OBJ)/csisatMatrix.cmx $(OBJ)/csisatLIUtils.cmx \
++	$(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatSatPL.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatPicoInterface.cmo \
++	$(OBJ)/csisatNelsonOppen.cmo $(OBJ)/csisatDpllProof.cmo \
++	$(OBJ)/csisatDpllCore.cmo $(OBJ)/csisatDpllClause.cmo \
++	$(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatSatPL.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatPicoInterface.cmx \
++	$(OBJ)/csisatNelsonOppen.cmx $(OBJ)/csisatDpllProof.cmx \
++	$(OBJ)/csisatDpllCore.cmx $(OBJ)/csisatDpllClause.cmx \
++	$(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatSatUIF.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \
++	$(OBJ)/csisatMessage.cmo $(OBJ)/csisatDag.cmo \
++	$(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo
++$(OBJ)/csisatSatUIF.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \
++	$(OBJ)/csisatMessage.cmx $(OBJ)/csisatDag.cmx \
++	$(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx
++$(OBJ)/csisatTests.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatUIF.cmo \
++	$(OBJ)/csisatSatPL.cmo $(OBJ)/csisatSatLI.cmo \
++	$(OBJ)/csisatNelsonOppen.cmo $(OBJ)/csisatMessage.cmo \
++	$(OBJ)/csisatLIUtils.cmo $(OBJ)/csisatInterpolate.cmo \
++	$(OBJ)/csisatFociPrinter.cmo $(OBJ)/csisatAstUtil.cmo \
++	$(OBJ)/csisatAst.cmo
++$(OBJ)/csisatTests.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatUIF.cmx \
++	$(OBJ)/csisatSatPL.cmx $(OBJ)/csisatSatLI.cmx \
++	$(OBJ)/csisatNelsonOppen.cmx $(OBJ)/csisatMessage.cmx \
++	$(OBJ)/csisatLIUtils.cmx $(OBJ)/csisatInterpolate.cmx \
++	$(OBJ)/csisatFociPrinter.cmx $(OBJ)/csisatAstUtil.cmx \
++	$(OBJ)/csisatAst.cmx
+diff -up ./pico_ml_wrapper/Makefile.ORIG ./pico_ml_wrapper/Makefile
+--- ./pico_ml_wrapper/Makefile.ORIG	2008-07-08 22:38:01.000000000 -0600
++++ ./pico_ml_wrapper/Makefile	2010-01-19 14:16:01.399524477 -0700
+@@ -1,7 +1,7 @@
+ CC=gcc
+ CFLAGS= -O2 -Wall
+-INCLUDE= -I../picosat-632
+-LIBS= -lpicosat -L../picosat-632
++INCLUDE=
++LIBS= -lpicosat
+ RM = /bin/rm -f
+ 
+ SRC = src/camlpico.c
diff --git a/csisat.spec b/csisat.spec
new file mode 100644
index 0000000..b19a96c
--- /dev/null
+++ b/csisat.spec
@@ -0,0 +1,74 @@
+Name:           csisat
+Version:        1.2
+Release:        2%{?dist}
+Summary:        Tool for LA+EUF Interpolation
+
+Group:          Applications/Engineering
+License:        ASL 2.0
+URL:            http://csisat.googlecode.com/
+Source0:        http://csisat.googlecode.com/files/%{name}-%{version}.zip
+# This patch has not been sent upstream.  Upstream wishes to distribute the
+# picosat sources with their code.  This patch builds with the system picosat
+# instead, and also adds missing dependencies so that parallel make works.
+Patch0:         csisat-makefile.patch
+BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
+
+BuildRequires:  glpk-devel, ocaml, picosat-devel
+
+# Exclude arches where ocaml is not available
+ExcludeArch:    sparc64 s390 s390x
+
+# Use the Ocaml dependency generators
+%global _use_internal_dependency_generator 0
+%global __find_requires /usr/lib/rpm/ocaml-find-requires.sh
+%global __find_provides /usr/lib/rpm/ocaml-find-provides.sh
+
+%description
+CSIsat reads a set of mathematical formulas that may combine variables,
+addition, multiplication, comparisons (<,>, etc.), as well as boolean
+expressions (and, or, not).  It determines if it is possible to set the
+variables to values so that the set of formulas are all simultaneously true
+(if it can, then the set of formulas is "satisfiable").
+
+More technically, CSIsat is an interpolating decision procedure for the
+quantifier-free theory of rational linear arithmetic (LA) and equality with
+uninterpreted function (EUF) symbols.  This implementation combines the
+efficiency of linear programming for solving the arithmetic part with the
+efficiency of a SAT solver to reason about the boolean structure.
+
+%prep
+%setup -q
+%patch0
+
+# Make sure we don't use the bundled version of picosat
+rm -fr picosat-*
+
+# Get rid of inappropriate executable bits
+chmod a-x *.txt
+find . -name \*.c | xargs chmod a-x
+
+%build
+make %{?_smp_mflags} \
+  CFLAGS="$RPM_OPT_FLAGS -I%{_libdir}/ocaml -I%{_includedir}/glpk"
+
+%install
+rm -rf $RPM_BUILD_ROOT
+mkdir -p $RPM_BUILD_ROOT%{_bindir}
+cp -p bin/* $RPM_BUILD_ROOT%{_bindir}
+
+%clean
+rm -rf $RPM_BUILD_ROOT
+
+%files
+%defattr(-,root,root,-)
+%doc License.txt License_Apache-2.0.txt ReadMe.txt ToDo.txt server/README
+%{_bindir}/csisat
+%{_bindir}/csisatServer
+
+%changelog
+* Tue Jan 19 2010 Jerry James <loganjerry@gmail.com> - 1.2-2
+- Fix parallel make
+- Less opaque description
+
+* Wed Sep  2 2009 Jerry James <loganjerry@gmail.com> - 1.2-1
+- Initial RPM
diff --git a/sources b/sources
index e69de29..f366332 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+fa0fec35362b452ba564f0f82086295f  csisat-1.2.zip