diff --git a/.cvsignore b/.cvsignore
index e69de29..f76e0d5 100644
--- a/.cvsignore
+++ b/.cvsignore
@@ -0,0 +1 @@
+cvc3-2.1.tar.gz
diff --git a/cvc3-build.patch b/cvc3-build.patch
new file mode 100644
index 0000000..58119f3
--- /dev/null
+++ b/cvc3-build.patch
@@ -0,0 +1,21 @@
+diff -dur cvc3-2.1.ORIG/Makefile.std cvc3-2.1/Makefile.std
+--- cvc3-2.1.ORIG/Makefile.std 2009-09-30 12:54:34.000000000 -0600
++++ cvc3-2.1/Makefile.std 2009-10-15 21:12:35.804289073 -0600
+@@ -92,7 +92,7 @@
+ DEBUG_PLATFORM = -optdbg
+ else
+ ifeq ($(OPTIMIZED),1)
+- LOCAL_CXXFLAGS = -O2
++ LOCAL_CXXFLAGS =
+ DEBUG_PLATFORM =
+ else
+ LOCAL_CXXFLAGS = -D_CVC3_DEBUG_MODE -g -O0
+@@ -177,7 +177,7 @@
+ BUILD_SHARED_LIB=1
+ endif
+
+-LOCAL_CXXFLAGS += -Wall $(INCLUDE_DIR)
++LOCAL_CXXFLAGS += $(INCLUDE_DIR)
+
+ ifdef EXTRAFLAGS
+ LOCAL_CXXFLAGS += $(EXTRAFLAGS)
diff --git a/cvc3-doc.patch b/cvc3-doc.patch
new file mode 100644
index 0000000..646559a
--- /dev/null
+++ b/cvc3-doc.patch
@@ -0,0 +1,666 @@
+diff -dur cvc3-2.1.ORIG/doc/Doxyfile.in cvc3-2.1/doc/Doxyfile.in
+--- cvc3-2.1.ORIG/doc/Doxyfile.in 2007-09-12 18:06:50.000000000 -0600
++++ cvc3-2.1/doc/Doxyfile.in 2009-10-19 10:13:12.768107753 -0600
+@@ -31,7 +31,7 @@
+ # This could be handy for archiving the generated documentation or
+ # if some version control system is used.
+
+-PROJECT_NUMBER =
++PROJECT_NUMBER = 2.1
+
+ # The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute)
+ # base path where the generated documentation will be put.
+@@ -499,8 +499,7 @@
+ # excluded from the INPUT source files. This way you can easily exclude a
+ # subdirectory from a directory tree whose root is specified with the INPUT tag.
+
+-EXCLUDE = devel.dox \
+- theory_api.dox
++EXCLUDE = devel.dox
+
+ # The EXCLUDE_SYMLINKS tag can be used select whether or not files or
+ # directories that are symbolic links (a Unix filesystem feature) are excluded
+@@ -1042,8 +1041,7 @@
+ # undefined via #undef or recursively expanded use the := operator
+ # instead of the = operator.
+
+-PREDEFINED = DEBUG \
+- DOXYGEN
++PREDEFINED = DOXYGEN
+
+ # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then
+ # this tag can be used to specify a list of macro names that should be expanded.
+@@ -1137,6 +1135,24 @@
+
+ HAVE_DOT = @HAVE_DOT@
+
++# By default doxygen will write a font called FreeSans.ttf to the output
++# directory and reference it in all dot files that doxygen generates. This
++# font does not include all possible unicode characters however, so when you need
++# these (or just want a differently looking font) you can specify the font name
++# using DOT_FONTNAME. You need need to make sure dot is able to find the font,
++# which can be done by putting it in a standard location or by setting the
++# DOTFONTPATH environment variable or by setting DOT_FONTPATH to the directory
++# containing the font.
++
++DOT_FONTNAME = FreeSans
++
++# By default doxygen will tell dot to use the output directory to look for the
++# FreeSans.ttf font (which doxygen will put there itself). If you specify a
++# different font using DOT_FONTNAME you can set the path where dot
++# can find it using this tag.
++
++DOT_FONTPATH = /usr/share/fonts/gnu-free
++
+ # If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen
+ # will generate a graph for each documented class showing the direct and
+ # indirect inheritance relations. Setting this tag to YES will force the
+@@ -1213,7 +1229,7 @@
+ # generated by dot. Possible values are png, jpg, or gif
+ # If left blank png will be used.
+
+-DOT_IMAGE_FORMAT = gif
++DOT_IMAGE_FORMAT = png
+
+ # The tag DOT_PATH can be used to specify the path where the dot tool can be
+ # found. If left blank, it is assumed the dot tool can be found in the path.
+@@ -1247,7 +1263,7 @@
+ # makes dot run faster, but since only newer versions of dot (>1.8.10)
+ # support this, this feature is disabled by default.
+
+-DOT_MULTI_TARGETS = NO
++DOT_MULTI_TARGETS = YES
+
+ # If the GENERATE_LEGEND tag is set to YES (the default) Doxygen will
+ # generate a legend page explaining the meaning of the various boxes and
+diff -dur cvc3-2.1.ORIG/INSTALL cvc3-2.1/INSTALL
+--- cvc3-2.1.ORIG/INSTALL 2009-10-15 16:06:18.000000000 -0600
++++ cvc3-2.1/INSTALL 2009-10-19 10:13:59.048162819 -0600
+@@ -196,7 +196,7 @@
+
+
+ Note: The Java interface depends on the "build type" (e.g.,
+-"optimized", "debug) of %CVC3. If you choose to re-configure and
++"optimized", "debug") of %CVC3. If you choose to re-configure and
+ re-build %CVC3 with a different build type, you must run "make clean"
+ in the current directory and re-build the interface (cleaning and
+ rebuilding the entire %CVC3 package will suffice).
+diff -dur cvc3-2.1.ORIG/src/include/expr.h cvc3-2.1/src/include/expr.h
+--- cvc3-2.1.ORIG/src/include/expr.h 2009-10-04 12:41:29.000000000 -0600
++++ cvc3-2.1/src/include/expr.h 2009-10-19 10:13:37.775165727 -0600
+@@ -388,7 +388,7 @@
+ //! Test if e is an atomic formula
+ /*! An atomic formula is TRUE or FALSE or an application of a predicate
+ (possibly 0-ary) which does not properly contain any formula. For
+- instance, the formula "x = IF f THEN y ELSE z ENDIF is not an atomic
++ instance, the formula "x = IF f THEN y ELSE z ENDIF" is not an atomic
+ formula, since it contains the condition "f", which is a formula. */
+ bool isAtomicFormula() const;
+ //! An abstract atomic formua is an atomic formula or a quantified formula
+diff -dur cvc3-2.1.ORIG/src/include/theory_arith3.h cvc3-2.1/src/include/theory_arith3.h
+--- cvc3-2.1.ORIG/src/include/theory_arith3.h 2009-05-29 23:48:15.000000000 -0600
++++ cvc3-2.1/src/include/theory_arith3.h 2009-10-19 10:13:12.769107906 -0600
+@@ -337,7 +337,7 @@
+ * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
+ * changes in the future, it will not be used in the ordering.
+ *
+- * @param var the variable
++ * @param variable the variable
+ * @param max the value to set it to
+ */
+ void fixCurrentMaxCoefficient(Expr variable, Rational max);
+diff -dur cvc3-2.1.ORIG/src/include/theory_arith_new.h cvc3-2.1/src/include/theory_arith_new.h
+--- cvc3-2.1.ORIG/src/include/theory_arith_new.h 2009-06-29 20:14:48.000000000 -0600
++++ cvc3-2.1/src/include/theory_arith_new.h 2009-10-19 10:13:12.769107906 -0600
+@@ -434,7 +434,7 @@
+ inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
+
+ /**
+- * Les then or equal comparison operator.
++ * Less than or equal comparison operator.
+ */
+ inline bool operator <= (const EpsRational& r) const {
+ switch (r.type) {
+@@ -459,12 +459,12 @@
+ }
+
+ /**
+- * Les then comparison operator.
++ * Less than comparison operator.
+ */
+ inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
+
+ /**
+- * Bigger then equal comparison operator.
++ * Greater than comparison operator.
+ */
+ inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
+
+@@ -787,6 +787,7 @@
+ * Asserts a new upper bound constraint on a variable and performs a simple check for consistency (not complete).
+ *
+ * @param x_i the variable to assert the bound on
++ * @param c the bound to assert
+ */
+ QueryResult assertUpper(const Expr& x_i, const EpsRational& c, const Theorem& thm);
+
+@@ -794,13 +795,15 @@
+ * Asserts a new lower bound constraint on a variable and performs a simple check for consistency (not complete).
+ *
+ * @param x_i the variable to assert the bound on
++ * @param c the bound to assert
+ */
+ QueryResult assertLower(const Expr& x_i, const EpsRational& c, const Theorem& thm);
+
+ /**
+- * Asserts a new equality constraint on a variable by asserting both upper and lower bound.
++ * Asserts a new equality constraint on a variable by asserting both upper and lower bounds.
+ *
+ * @param x_i the variable to assert the bound on
++ * @param c the the bound to assert
+ */
+ QueryResult assertEqual(const Expr& x_i, const EpsRational& c, const Theorem& thm);
+
+@@ -862,8 +865,8 @@
+
+ /**
+ * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
+- * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separatied to
+- *
++ * explanation clause. The variables in the row of \f$x_i = \sum_x{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to
++ *
+ * - \f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
+ *
- \f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$
+ *
+@@ -878,7 +881,7 @@
+
+ /**
+ * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
+- * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separatied to
++ * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to
+ *
+ * - \f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
+ *
- \f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$
+diff -dur cvc3-2.1.ORIG/src/include/theory_arith_old.h cvc3-2.1/src/include/theory_arith_old.h
+--- cvc3-2.1.ORIG/src/include/theory_arith_old.h 2009-09-29 19:50:21.000000000 -0600
++++ cvc3-2.1/src/include/theory_arith_old.h 2009-10-19 10:13:12.771175241 -0600
+@@ -364,7 +364,7 @@
+ * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
+ * changes in the future, it will not be used in the ordering.
+ *
+- * @param var the variable
++ * @param variable the variable
+ * @param max the value to set it to
+ */
+ void fixCurrentMaxCoefficient(Expr variable, Rational max);
+@@ -653,7 +653,7 @@
+ inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
+
+ /**
+- * Les then or equal comparison operator.
++ * Less than or equal comparison operator.
+ */
+ inline bool operator <= (const EpsRational& r) const {
+ switch (r.type) {
+@@ -678,19 +678,19 @@
+ }
+
+ /**
+- * Les then comparison operator.
++ * Less than comparison operator.
+ */
+ inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
+
+ /**
+- * Bigger then equal comparison operator.
++ * Greater than comparison operator.
+ */
+ inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
+
+ /**
+ * Returns the string representation of the number.
+ *
+- * @param the string representation of the number
++ * @return the string representation of the number
+ */
+ std::string toString() const {
+ switch (type) {
+@@ -846,7 +846,6 @@
+ * @param x variable x::Difference
+ * @param y variable y
+ * @param c rational c
+- * @param kind the kind of inequality (LE or LT)
+ * @param edge_thm the theorem for this edge
+ */
+ void addEdge(const Expr& x, const Expr& y, const Rational& c, const Theorem& edge_thm);
+diff -dur cvc3-2.1.ORIG/src/include/vc.h cvc3-2.1/src/include/vc.h
+--- cvc3-2.1.ORIG/src/include/vc.h 2009-10-04 12:41:29.000000000 -0600
++++ cvc3-2.1/src/include/vc.h 2009-10-19 10:13:12.772197964 -0600
+@@ -28,9 +28,7 @@
+ #include "formula_value.h"
+
+ /*****************************************************************************/
+-/*!
+- *\defgroup Note Note that this list of modules is very incomplete
+- *\brief Note that this list of modules is very incomplete
++/*! Note that this list of modules is very incomplete
+ */
+ /*****************************************************************************/
+
+@@ -750,10 +748,10 @@
+
+ //! Set triggers for quantifier instantiation
+ /*!
+- * \param e is the expression for which triggers are being set. \param
+- * Each item in triggers is a vector of Expr containing one or more
+- * patterns. A pattern is a term or Atomic predicate sub-expression of
+- * e. A vector containing more than one pattern is treated as a
++ * \param e the expression for which triggers are being set
++ * \param triggers Each item in triggers is a vector of Expr containing one
++ * or more patterns. A pattern is a term or Atomic predicate sub-expression
++ * of e. A vector containing more than one pattern is treated as a
+ * multi-trigger. Patterns will be matched in the order they occur in
+ * the vector.
+ */
+diff -dur cvc3-2.1.ORIG/src/sat/sat_proof.h cvc3-2.1/src/sat/sat_proof.h
+--- cvc3-2.1.ORIG/src/sat/sat_proof.h 2008-04-03 22:18:32.000000000 -0600
++++ cvc3-2.1/src/sat/sat_proof.h 2009-10-19 10:13:12.773204281 -0600
+@@ -1,6 +1,6 @@
+ /*****************************************************************************/
+ /*!
+- *\file minisat_proof.h
++ *\file sat_proof.h
+ *\brief Sat solver proof representation
+ *
+ * Author: Alexander Fuchs
+diff -dur cvc3-2.1.ORIG/src/theory_arith/theory_arith3.cpp cvc3-2.1/src/theory_arith/theory_arith3.cpp
+--- cvc3-2.1.ORIG/src/theory_arith/theory_arith3.cpp 2009-10-08 16:15:52.000000000 -0600
++++ cvc3-2.1/src/theory_arith/theory_arith3.cpp 2009-10-19 10:13:12.775109510 -0600
+@@ -421,7 +421,7 @@
+ return thm;
+ }
+
+-/*! Psuedo-code for doSolve. (Input is an equation) (output is a Theorem)
++/*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
+ * -# translate e to the form e' = 0
+ * -# if (e'.isRational()) then {if e' != 0 return false else true}
+ * -# a for loop checks if all the variables are integers.
+diff -dur cvc3-2.1.ORIG/src/theory_arith/theory_arith_new.cpp cvc3-2.1/src/theory_arith/theory_arith_new.cpp
+--- cvc3-2.1.ORIG/src/theory_arith/theory_arith_new.cpp 2009-10-08 16:15:52.000000000 -0600
++++ cvc3-2.1/src/theory_arith/theory_arith_new.cpp 2009-10-19 10:13:12.777233052 -0600
+@@ -320,7 +320,7 @@
+ return thm;
+ }
+
+-/*! Psuedo-code for doSolve. (Input is an equation) (output is a Theorem)
++/*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
+ * -# translate e to the form e' = 0
+ * -# if (e'.isRational()) then {if e' != 0 return false else true}
+ * -# a for loop checks if all the variables are integers.
+diff -dur cvc3-2.1.ORIG/src/theory_arith/theory_arith_old.cpp cvc3-2.1/src/theory_arith/theory_arith_old.cpp
+--- cvc3-2.1.ORIG/src/theory_arith/theory_arith_old.cpp 2009-10-08 16:15:52.000000000 -0600
++++ cvc3-2.1/src/theory_arith/theory_arith_old.cpp 2009-10-19 10:13:12.781233049 -0600
+@@ -436,7 +436,7 @@
+ return thm;
+ }
+
+-/*! Psuedo-code for doSolve. (Input is an equation) (output is a Theorem)
++/*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
+ * -# translate e to the form e' = 0
+ * -# if (e'.isRational()) then {if e' != 0 return false else true}
+ * -# a for loop checks if all the variables are integers.
+diff -dur cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp
+--- cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-15 19:23:59.000000000 -0600
++++ cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-19 10:13:12.785232967 -0600
+@@ -479,7 +479,7 @@
+
+ //if both MSBs are constants, then we can optimize the output. we
+ //know precisely the value of the signed comparison in cases where
+- //topbit of e0 and e1 are constants. e.g. |-1@t0 < 0@t1 is clearly
++ //topbit of e0 and e1 are constants. e.g. |-1\@t0 < 0\@t1 is clearly
+ //|-TRUE.
+
+ //-1 indicates that both topBits are not known to be BVCONSTS
+@@ -1009,9 +1009,9 @@
+ }
+
+
+-// Input: x: a_0 @ ... @ a_n,
++// Input: x: a_0 \@ ... \@ a_n,
+ // i: bitposition
+-// Output |- BOOLEXTRACT(a_0 @ ... @ a_n, i) <=> BOOLEXTRACT(a_j, k)
++// Output |- BOOLEXTRACT(a_0 \@ ... \@ a_n, i) <=> BOOLEXTRACT(a_j, k)
+ // where j and k are determined by structure of CONCAT
+ Theorem BitvectorTheoremProducer::bitExtractConcatenation(const Expr & x,
+ int i)
+@@ -1939,7 +1939,7 @@
+ }
+
+
+-//! t<>m = 0bin00...00 @ t[bvLength-1:m], takes e == (t>>n)
++//! t>>m = 0bin00...00 \@ t[bvLength-1:m], takes e == (t>>n)
+ Theorem BitvectorTheoremProducer::rightShiftToConcat(const Expr& e) {
+ if(CHECK_PROOFS) {
+ CHECK_SOUND(e.getOpKind() == RIGHTSHIFT && e.arity() == 1,
+@@ -2028,7 +2028,7 @@
+ }
+
+
+-//! BVSHL(t,c) = t[n-c,0] @ 0bin00...00
++//! BVSHL(t,c) = t[n-c,0] \@ 0bin00...00
+ Theorem BitvectorTheoremProducer::bvshlToConcat(const Expr& e) {
+ if(CHECK_PROOFS) {
+ // The second kid must be a constant expression
+@@ -2102,7 +2102,7 @@
+ }
+
+
+-//! BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]
++//! BVLSHR(t,c) = 0bin00...00 \@ t[n-1,c]
+ Theorem BitvectorTheoremProducer::bvlshrToConcat(const Expr& e)
+ {
+ if(CHECK_PROOFS) {
+@@ -2265,7 +2265,7 @@
+
+
+ //! k*t = BVPLUS(n, ) -- translation of k*t to BVPLUS
+-/*! If k = 2^m, return k*t = t@0...0 */
++/*! If k = 2^m, return k*t = t\@0...0 */
+ Theorem BitvectorTheoremProducer::constMultToPlus(const Expr& e) {
+ DebugAssert(false,
+ "BitvectorTheoremProducer::constMultToPlus: this rule does not work\n");
+@@ -2459,7 +2459,7 @@
+ }
+
+
+-//! (t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
++//! (t1 \@ t2)[i:j] = t1[...] \@ t2[...] (push extraction through concat)
+ Theorem
+ BitvectorTheoremProducer::extractConcat(const Expr& e) {
+ TRACE("bitvector rules", "extractConcat(", e, ") {");
+@@ -2672,7 +2672,7 @@
+ }
+
+
+-//! ~(t1@...@tn) = (~t1)@...@(~tn) -- push negation through concat
++//! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat
+ Theorem
+ BitvectorTheoremProducer::negConcat(const Expr& e) {
+ if(CHECK_PROOFS) {
+@@ -3190,7 +3190,7 @@
+ }
+
+
+-//! c1@c2@...@cn = c (concatenation of constant bitvectors)
++//! c1\@c2\@...\@cn = c (concatenation of constant bitvectors)
+ Theorem BitvectorTheoremProducer::concatConst(const Expr& e) {
+ if(CHECK_PROOFS) {
+ // The kids must be constant expressions
+@@ -3211,7 +3211,7 @@
+ }
+
+
+-//! Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w
++//! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w
+ Theorem
+ BitvectorTheoremProducer::concatFlatten(const Expr& e) {
+ if(CHECK_PROOFS) {
+@@ -3233,7 +3233,7 @@
+ }
+
+
+-//! Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0]
++//! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0]
+ Theorem
+ BitvectorTheoremProducer::concatMergeExtract(const Expr& e) {
+ if(CHECK_PROOFS) {
+@@ -4681,7 +4681,7 @@
+ }
+
+
+-// BVMULT(N, a@b, y) = BVPLUS(N, BVMULT(N,b,y), BVMULT(N-n,a,y) @ n-bit-0-string)
++// BVMULT(N, a\@b, y) = BVPLUS(N, BVMULT(N,b,y), BVMULT(N-n,a,y) \@ n-bit-0-string)
+ // where n = BVSize(b), a != 0, one of a or b is a constant
+ Theorem BitvectorTheoremProducer::liftConcatBVMult(const Expr& e)
+ {
+@@ -4917,7 +4917,7 @@
+ }
+
+
+-// BVPLUS(N, a0, ..., an) = BVPLUS(N-n,a0[N-1:n],...an[N-1:n])@t
++// BVPLUS(N, a0, ..., an) = BVPLUS(N-n,a0[N-1:n],...an[N-1:n])\@t
+ // where n = BVSize(t), and the sum of the lowest n bits of a0..an is exactly
+ // equal to t (i.e. no carry)
+ Theorem BitvectorTheoremProducer::liftConcatBVPlus(const Expr& e)
+@@ -5602,9 +5602,9 @@
+
+ // Input: t[hi:lo] = rhs
+ // if t appears as leaf in rhs, then:
+-// t[hi:lo] = rhs |- Exists x,y,z. (t = x @ y @ z AND y = rhs), solvedForm = false
++// t[hi:lo] = rhs |- Exists x,y,z. (t = x \@ y i@ z AND y = rhs), solvedForm = false
+ // else
+-// t[hi:lo] = rhs |- Exists x,z. (t = x @ rhs @ z), solvedForm = true
++// t[hi:lo] = rhs |- Exists x,z. (t = x \@ rhs \@ z), solvedForm = true
+ Theorem BitvectorTheoremProducer::processExtract(const Theorem& e, bool& solvedForm)
+ {
+ Expr expr = e.getExpr();
+@@ -6075,7 +6075,7 @@
+ }
+
+
+-//! BVZEROEXTEND(e, i) = zeroString @ e
++//! BVZEROEXTEND(e, i) = zeroString \@ e
+ // where zeroString is a string of i zeroes
+ Theorem BitvectorTheoremProducer::zeroExtendRule(const Expr& e) {
+ if(CHECK_PROOFS) {
+@@ -6103,7 +6103,7 @@
+ }
+
+
+-//! BVREPEAT(e, i) = e @ e @ ... @ e
++//! BVREPEAT(e, i) = e \@ e \@ ... \@ e
+ // where e appears i times on the right
+ Theorem BitvectorTheoremProducer::repeatRule(const Expr& e) {
+ if(CHECK_PROOFS) {
+@@ -6136,7 +6136,7 @@
+ }
+
+
+-//! BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i]
++//! BVROTL(e, i) = a[n-i-1:0] \@ a[n-1:n-i]
+ // where n is the size of e and i is less than n (otherwise i mod n is used)
+ Theorem BitvectorTheoremProducer::rotlRule(const Expr& e) {
+ if(CHECK_PROOFS) {
+@@ -6167,7 +6167,7 @@
+ }
+
+
+-//! BVROTR(e, i) = a[i-1:0] @ a[n-1:i]
++//! BVROTR(e, i) = a[i-1:0] \@ a[n-1:i]
+ // where n is the size of e and i is less than n (otherwise i mod n is used)
+ Theorem BitvectorTheoremProducer::rotrRule(const Expr& e) {
+ if(CHECK_PROOFS) {
+diff -dur cvc3-2.1.ORIG/src/theory_core/theory_core.cpp cvc3-2.1/src/theory_core/theory_core.cpp
+--- cvc3-2.1.ORIG/src/theory_core/theory_core.cpp 2009-09-30 13:39:06.000000000 -0600
++++ cvc3-2.1/src/theory_core/theory_core.cpp 2009-10-19 10:13:12.788233008 -0600
+@@ -3099,7 +3099,7 @@
+ }
+
+
+-bool TheoryCore::incomplete(vector& reasons)
++bool TheoryCore::incomplete(std::vector& reasons)
+ {
+ if(d_incomplete.size() > 0) {
+ for(CDMap::iterator i=d_incomplete.begin(),
+diff -dur cvc3-2.1.ORIG/src/theory_datatype/theory_datatype.cpp cvc3-2.1/src/theory_datatype/theory_datatype.cpp
+--- cvc3-2.1.ORIG/src/theory_datatype/theory_datatype.cpp 2009-10-05 20:12:41.000000000 -0600
++++ cvc3-2.1/src/theory_datatype/theory_datatype.cpp 2009-10-19 10:13:12.790252403 -0600
+@@ -857,10 +857,10 @@
+ }
+
+
+-Expr TheoryDatatype::dataType(const string& name,
+- const vector& constructors,
+- const vector >& selectors,
+- const vector >& types)
++Expr TheoryDatatype::dataType(const std::string& name,
++ const std::vector& constructors,
++ const std::vector >& selectors,
++ const std::vector >& types)
+ {
+ vector names;
+ vector > constructors2;
+@@ -876,10 +876,10 @@
+
+ // Elements of types are either the expr from an existing type or a string
+ // naming one of the datatypes being defined
+-Expr TheoryDatatype::dataType(const vector& names,
+- const vector >& allConstructors,
+- const vector > >& allSelectors,
+- const vector > >& allTypes)
++Expr TheoryDatatype::dataType(const std::vector& names,
++ const std::vector >& allConstructors,
++ const std::vector > >& allSelectors,
++ const std::vector > >& allTypes)
+ {
+ vector returnTypes;
+
+diff -dur cvc3-2.1.ORIG/src/theory_quant/quant_theorem_producer.cpp cvc3-2.1/src/theory_quant/quant_theorem_producer.cpp
+--- cvc3-2.1.ORIG/src/theory_quant/quant_theorem_producer.cpp 2009-10-04 12:41:29.000000000 -0600
++++ cvc3-2.1/src/theory_quant/quant_theorem_producer.cpp 2009-10-19 10:13:12.791296402 -0600
+@@ -241,6 +241,7 @@
+ * subtype predicates for the bound variables of the quanitfied expression.
+ * \param t1 is the quantifier (a Theorem)
+ * \param terms are the terms to instantiate.
++ * \param quantLevel the quantification level for the formula
+ */
+ Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector& terms, int quantLevel){
+
+diff -dur cvc3-2.1.ORIG/src/theory_quant/theory_quant.cpp cvc3-2.1/src/theory_quant/theory_quant.cpp
+--- cvc3-2.1.ORIG/src/theory_quant/theory_quant.cpp 2009-10-07 00:24:44.000000000 -0600
++++ cvc3-2.1/src/theory_quant/theory_quant.cpp 2009-10-19 10:13:12.795232784 -0600
+@@ -2860,7 +2860,7 @@
+ }
+
+
+-void TheoryQuant::setupTriggers(ExprMap* >*>& trig_maps, const Theorem& thm, size_t univs_id){
++void TheoryQuant::setupTriggers(ExprMap* >*>& trig_maps, const Theorem& thm, size_t univs_id){
+
+ // static std::vector libQuant;
+ const Expr& e = thm.getExpr();
+@@ -4137,7 +4137,7 @@
+ }
+
+ //match a gterm against all the trigs in d_allmap_trigs
+-void TheoryQuant::matchListNew(ExprMap*>*>& new_trigs,
++void TheoryQuant::matchListNew(ExprMap*>*>& new_trigs,
+ const CDList& glist,
+ size_t gbegin,
+ size_t gend){
+@@ -7984,7 +7984,7 @@
+ d_lastEqsUpdatePos.set(d_eqsUpdate.size());
+ }
+
+-void TheoryQuant::synCheckSat(ExprMap* >* >& new_trigs, bool fullEffort){
++void TheoryQuant::synCheckSat(ExprMap* >* >& new_trigs, bool fullEffort){
+
+ d_allout=false;
+
+diff -dur cvc3-2.1.ORIG/src/vcl/vcl.cpp cvc3-2.1/src/vcl/vcl.cpp
+--- cvc3-2.1.ORIG/src/vcl/vcl.cpp 2009-10-15 14:29:30.000000000 -0600
++++ cvc3-2.1/src/vcl/vcl.cpp 2009-10-19 10:13:12.798131491 -0600
+@@ -775,8 +775,8 @@
+ }
+
+
+-Type VCL::recordType(const vector& fields,
+- const vector& types)
++Type VCL::recordType(const std::vector& fields,
++ const std::vector& types)
+ {
+ DebugAssert(fields.size() == types.size(),
+ "VCL::recordType: number of fields is different \n"
+@@ -789,9 +789,10 @@
+ }
+
+
+-Type VCL::dataType(const string& name,
+- const string& constructor,
+- const vector& selectors, const vector& types)
++Type VCL::dataType(const std::string& name,
++ const std::string& constructor,
++ const std::vector& selectors,
++ const std::vector& types)
+ {
+ vector constructors;
+ constructors.push_back(constructor);
+@@ -806,10 +807,10 @@
+ }
+
+
+-Type VCL::dataType(const string& name,
+- const vector& constructors,
+- const vector >& selectors,
+- const vector >& types)
++Type VCL::dataType(const std::string& name,
++ const std::vector& constructors,
++ const std::vector >& selectors,
++ const std::vector >& types)
+ {
+ Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);
+ if(d_dump) {
+@@ -819,11 +820,11 @@
+ }
+
+
+-void VCL::dataType(const vector& names,
+- const vector >& constructors,
+- const vector > >& selectors,
+- const vector > >& types,
+- vector& returnTypes)
++void VCL::dataType(const std::vector& names,
++ const std::vector >& constructors,
++ const std::vector > >& selectors,
++ const std::vector > >& types,
++ std::vector& returnTypes)
+ {
+ Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);
+ if(d_dump) {
+@@ -1405,8 +1406,8 @@
+ }
+
+
+-Expr VCL::recordExpr(const vector& fields,
+- const vector& exprs)
++Expr VCL::recordExpr(const std::vector& fields,
++ const std::vector& exprs)
+ {
+ DebugAssert(fields.size() > 0, "VCL::recordExpr()");
+ DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
+@@ -2107,7 +2108,7 @@
+ }
+
+
+-bool VCL::incomplete(vector& reasons) {
++bool VCL::incomplete(std::vector& reasons) {
+ // TODO: add to interactive interface
+ // Return true only after a failed query
+ return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
diff --git a/cvc3-gcc4.patch b/cvc3-gcc4.patch
new file mode 100644
index 0000000..cb66593
--- /dev/null
+++ b/cvc3-gcc4.patch
@@ -0,0 +1,80 @@
+diff -dur cvc3-2.1.ORIG/src/include/command_line_exception.h cvc3-2.1/src/include/command_line_exception.h
+--- cvc3-2.1.ORIG/src/include/command_line_exception.h 2006-08-09 15:19:30.000000000 -0600
++++ cvc3-2.1/src/include/command_line_exception.h 2009-10-16 09:34:46.141974605 -0600
+@@ -31,7 +31,7 @@
+ // Constructors
+ CLException() { }
+ CLException(const std::string& msg): Exception(msg) { }
+- CLException(char* msg): Exception(msg) { }
++ CLException(const char* msg): Exception(msg) { }
+ // Destructor
+ virtual ~CLException() { }
+ // Printing the message
+diff -dur cvc3-2.1.ORIG/src/include/memory_manager_context.h cvc3-2.1/src/include/memory_manager_context.h
+--- cvc3-2.1.ORIG/src/include/memory_manager_context.h 2009-04-10 14:38:25.000000000 -0600
++++ cvc3-2.1/src/include/memory_manager_context.h 2009-10-16 09:34:46.141974605 -0600
+@@ -21,6 +21,7 @@
+ #ifndef _cvc3__include__memory_manager_context_h
+ #define _cvc3__include__memory_manager_context_h
+
++#include
+ #include
+ #include "memory_manager.h"
+
+diff -dur cvc3-2.1.ORIG/src/include/sound_exception.h cvc3-2.1/src/include/sound_exception.h
+--- cvc3-2.1.ORIG/src/include/sound_exception.h 2006-08-09 15:19:30.000000000 -0600
++++ cvc3-2.1/src/include/sound_exception.h 2009-10-16 09:34:46.142839030 -0600
+@@ -33,7 +33,7 @@
+ // Constructors
+ SoundException() { }
+ SoundException(const std::string& msg): Exception(msg) { }
+- SoundException(char* msg): Exception(msg) { }
++ SoundException(const char* msg): Exception(msg) { }
+ // Destructor
+ virtual ~SoundException() { }
+ virtual std::string toString() const {
+diff -dur cvc3-2.1.ORIG/src/theory_arith/arith_exception.h cvc3-2.1/src/theory_arith/arith_exception.h
+--- cvc3-2.1.ORIG/src/theory_arith/arith_exception.h 2006-08-09 15:19:31.000000000 -0600
++++ cvc3-2.1/src/theory_arith/arith_exception.h 2009-10-16 09:35:47.378849519 -0600
+@@ -35,7 +35,7 @@
+ // Constructors
+ ArithException() { }
+ ArithException(const std::string& msg): Exception(msg) { }
+- ArithException(char* msg): Exception(msg) { }
++ ArithException(const char* msg): Exception(msg) { }
+ // Destructor
+ virtual ~ArithException() { }
+ virtual std::string toString() const {
+diff -dur cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp
+--- cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-16 09:34:37.696911611 -0600
++++ cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-16 09:36:54.411809170 -0600
+@@ -28,6 +28,7 @@
+ // This code is trusted
+ #define _CVC3_TRUSTED_
+
++#include
+ #include "bitvector_theorem_producer.h"
+ #include "common_proof_rules.h"
+ #include "theory_core.h"
+diff -dur cvc3-2.1.ORIG/src/util/debug.cpp cvc3-2.1/src/util/debug.cpp
+--- cvc3-2.1.ORIG/src/util/debug.cpp 2009-03-03 10:31:33.000000000 -0700
++++ cvc3-2.1/src/util/debug.cpp 2009-10-16 09:34:46.144161887 -0600
+@@ -19,6 +19,7 @@
+ */
+ /*****************************************************************************/
+
++#include
+ #include
+ #include
+
+diff -dur cvc3-2.1.ORIG/src/util/rational-gmp.cpp cvc3-2.1/src/util/rational-gmp.cpp
+--- cvc3-2.1.ORIG/src/util/rational-gmp.cpp 2008-11-14 13:49:11.000000000 -0700
++++ cvc3-2.1/src/util/rational-gmp.cpp 2009-10-16 09:34:46.145125371 -0600
+@@ -24,6 +24,7 @@
+ #include "compat_hash_set.h"
+ #include "rational.h"
+
++#include
+ #include
+ #include
+ #include
diff --git a/cvc3-java.patch b/cvc3-java.patch
new file mode 100644
index 0000000..740d4d7
--- /dev/null
+++ b/cvc3-java.patch
@@ -0,0 +1,60 @@
+diff -dur cvc3-2.1.ORIG/java/include/cvc3/JniUtils.h cvc3-2.1/java/include/cvc3/JniUtils.h
+--- cvc3-2.1.ORIG/java/include/cvc3/JniUtils.h 2008-12-12 15:48:14.000000000 -0700
++++ cvc3-2.1/java/include/cvc3/JniUtils.h 2009-10-19 11:22:57.817991587 -0600
+@@ -168,7 +168,7 @@
+ env->FindClass("java/lang/Object"),
+ NULL);
+
+- for (int i = 0; i < v.size(); ++i) {
++ for (unsigned int i = 0U; i < v.size(); ++i) {
+ env->SetObjectArrayElement(jarray, i, embed_copy(env, v[i]));
+ }
+
+@@ -182,7 +182,7 @@
+ env->FindClass("java/lang/Object"),
+ NULL);
+
+- for (int i = 0; i < v.size(); ++i) {
++ for (unsigned int i = 0U; i < v.size(); ++i) {
+ env->SetObjectArrayElement(jarray, i, embed_const_ref(env, &v[i]));
+ }
+
+diff -dur cvc3-2.1.ORIG/java/src/cvc3/JniUtils.cpp cvc3-2.1/java/src/cvc3/JniUtils.cpp
+--- cvc3-2.1.ORIG/java/src/cvc3/JniUtils.cpp 2008-10-01 12:35:31.000000000 -0600
++++ cvc3-2.1/java/src/cvc3/JniUtils.cpp 2009-10-19 11:22:17.203023038 -0600
+@@ -74,6 +74,9 @@
+ case PRESENTATION_LANG: return toJava(env, "PRESENTATION");
+ case SMTLIB_LANG: return toJava(env, "SMTLIB");
+ case LISP_LANG: return toJava(env, "LISP");
++ case AST_LANG: return toJava(env, "AST");
++ case SIMPLIFY_LANG: return toJava(env, "SIMPLIFY");
++ case TPTP_LANG: return toJava(env, "TPTP");
+ }
+
+ DebugAssert(false, "JniUtils::toJava(InputLanguage): unreachable");
+@@ -155,7 +158,7 @@
+ env->FindClass("java/lang/String"),
+ env->NewStringUTF(""));
+
+- for(int i = 0; i < v.size(); ++i) {
++ for(unsigned int i = 0U; i < v.size(); ++i) {
+ env->SetObjectArrayElement(jarray, i, toJava(env, v[i]));
+ }
+
+diff -dur cvc3-2.1.ORIG/java/src/cvc3/ValidityChecker_impl.cpp cvc3-2.1/java/src/cvc3/ValidityChecker_impl.cpp
+--- cvc3-2.1.ORIG/java/src/cvc3/ValidityChecker_impl.cpp 2009-09-30 12:54:35.000000000 -0600
++++ cvc3-2.1/java/src/cvc3/ValidityChecker_impl.cpp 2009-10-19 11:22:17.203023038 -0600
+@@ -584,11 +584,11 @@
+ return embed_copy(env, vc->forallExpr(vars, *body));
+
+ DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr2
+-jobject m ValidityChecker vc cv Expr vars c Expr body cv Expr triggers
++jobject m ValidityChecker vc cv Expr vars c Expr body cvv Expr triggers
+ return embed_copy(env, vc->forallExpr(vars, *body, triggers));
+
+ DEFINITION: Java_cvc3_ValidityChecker_jniSetTriggers
+-void m ValidityChecker vc c Expr closure cv Expr triggers
++void m ValidityChecker vc c Expr closure cvv Expr triggers
+ vc->setTriggers(*closure, triggers);
+
+ DEFINITION: Java_cvc3_ValidityChecker_jniExistsExpr
diff --git a/cvc3.spec b/cvc3.spec
new file mode 100644
index 0000000..5c960c7
--- /dev/null
+++ b/cvc3.spec
@@ -0,0 +1,248 @@
+# If the emacs-el package has installed a pkgconfig file, use that to determine
+# install locations and Emacs version at build time, otherwise set defaults.
+%if %($(pkg-config emacs) ; echo $?)
+%define emacs_version 22.1
+%define emacs_lispdir %{_datadir}/emacs/site-lisp
+%else
+%define emacs_version %(pkg-config emacs --modversion)
+%define emacs_lispdir %(pkg-config emacs --variable sitepkglispdir)
+%endif
+
+# If the xemacs-devel package has installed a pkgconfig file, use that to
+# determine install locations and Emacs version at build time, otherwise set
+# defaults.
+%if %($(pkg-config xemacs) ; echo $?)
+%define xemacs_version 21.5
+%define xemacs_lispdir %{_datadir}/xemacs/site-packages/lisp
+%else
+%define xemacs_version %(pkg-config xemacs --modversion)
+%define xemacs_lispdir %(pkg-config xemacs --variable sitepkglispdir)
+%endif
+
+Name: cvc3
+Version: 2.1
+Release: 2%{?dist}
+Summary: Validity checker of many-sorted first-order formulas with theories
+
+Group: Applications/Engineering
+License: BSD
+URL: http://www.cs.nyu.edu/acsys/cvc3/
+Source: http://www.cs.nyu.edu/acsys/cvc3/download/%{version}/cvc3-%{version}.tar.gz
+# Override compiler flag selection so that $RPM_OPT_FLAGS will take effect.
+# Submitted upstream June 2008.
+Patch0: cvc3-build.patch
+# Fix a few problems in the doxygen documentation.
+# Submitted upstream June 2008, with an update in August 2008.
+Patch1: cvc3-doc.patch
+# GCC 4.3+ uses a streamlined header architecture, so more includes are needed.
+# This patch was last submitted upstream on 16 Oct 2009.
+Patch2: cvc3-gcc4.patch
+BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
+# Fix Java build problems. This patch was last sent upstream on 19 Oct 2009.
+Patch3: cvc3-java.patch
+
+BuildRequires: bison, doxygen, emacs, emacs-el, flex, gnu-free-sans-fonts
+BuildRequires: gmp-devel, graphviz, java-devel, jpackage-utils, perl, time
+BuildRequires: transfig, tex(latex), xemacs, xemacs-devel
+Requires: gnu-free-sans-fonts
+
+%description
+CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT)
+problems. It can be used to prove the validity (or, dually, the
+satisfiability) of first-order formulas in a large number of built-in logical
+theories and their combination.
+
+CVC3 is the latest offspring of a series of popular SMT provers, which
+originated at Stanford University with the SVC system. In particular, it
+builds on the code base of CVC Lite, its most recent predecessor. Its high
+level design follows that of the Sammy prover.
+
+CVC3 works with a version of first-order logic with polymorphic types and has
+a wide variety of features including:
+
+ * several built-in base theories: rational and integer linear arithmetic,
+ arrays, tuples, records, inductive data types, bit vectors, and equality
+ over uninterpreted function symbols;
+ * support for quantifiers;
+ * an interactive text-based interface;
+ * a rich C and C++ API for embedding in other systems;
+ * proof and model generation abilities;
+ * predicate subtyping;
+ * essentially no limit on its use for research or commercial purposes (see
+ license).
+
+For example, if you run 'cvc3 +interactive' and submit:
+ i, j: INT; ASSERT i = j + 1; QUERY i>j;
+it will determine "Valid." If you then ask:
+ QUERY i= %{emacs_version}
+Requires: %{name} = %{version}-%{release}
+
+%description emacs
+This package contains the byte compiled CVC3 mode for Emacs.
+
+%package emacs-el
+Group: Applications/Engineering
+Summary: Elisp source files for the CVC3 Emacs mode
+Requires: %{name} = %{version}-%{release}
+
+%description emacs-el
+This package contains the source Elisp files for the CVC3 mode for Emacs. You
+do not need to install this package to run %{name}. Install the %{name}-emacs
+package to use %{name} with Emacs.
+
+%package xemacs
+Group: Applications/Engineering
+Summary: Compiled XEmacs mode for CVC3
+Requires: xemacs(bin) >= %{xemacs_version}
+Requires: %{name} = %{version}-%{release}
+
+%description xemacs
+This package contains the byte compiled CVC3 mode for XEmacs.
+
+%package xemacs-el
+Group: Applications/Engineering
+Summary: Elisp source files for the CVC3 XEmacs mode
+Requires: %{name} = %{version}-%{release}
+
+%description xemacs-el
+This package contains the source Elisp files for the CVC3 mode for XEmacs. You
+do not need to install this package to run %{name}. Install the %{name}-xemacs
+package to use %{name} with XEmacs.
+
+%prep
+%setup -q
+%patch0 -p1
+%patch1 -p1
+%patch2 -p1
+%patch3 -p1
+
+# We can't use loadLibrary, since the JNI libaries are not in a standard place
+sed -i \
+ -e "s|loadLibrary(\"cvc3jni\")|load(\"%{_libdir}/%{name}/libcvc3jni.so\")|" \
+ java/src/cvc3/Embedded.java
+
+%build
+%configure --with-build=optimized --enable-dynamic --enable-java \
+ --with-java-home=/usr/lib/jvm/java
+make %{?_smp_mflags}
+
+# Build the documentation
+cd doc
+make
+rm -f html/*.{map,md5}
+
+%install
+rm -rf %{buildroot}
+
+mkdir -p %{buildroot}%{_libdir}/%{name}
+%makeinstall javadir=%{buildroot}%{_libdir}/%{name}
+
+# Byte compile the CVC3 mode file for Emacs
+mkdir -p %{buildroot}%{_datadir}/emacs/site-lisp
+cp -p emacs/cvc-mode.el %{buildroot}%{_datadir}/emacs/site-lisp
+pushd %{buildroot}%{_datadir}/emacs/site-lisp
+emacs --batch --no-site-file -f batch-byte-compile cvc-mode.el
+popd
+
+# Byte compile the CVC3 mode file for XEmacs
+mkdir -p %{buildroot}%{_datadir}/xemacs/site-packages/lisp
+cp -p emacs/cvc-mode.el %{buildroot}%{_datadir}/xemacs/site-packages/lisp
+pushd %{buildroot}%{_datadir}/xemacs/site-packages/lisp
+xemacs --batch --no-site-file -f batch-byte-compile cvc-mode.el
+popd
+
+# Add missing executable bits to the shared libraries
+chmod a+x %{buildroot}%{_libdir}/*.so.*
+
+# Move the JNI libraries to the right place
+mv %{buildroot}%{_libdir}/libcvc3jni.* %{buildroot}%{_libdir}/%{name}
+
+# FIXME: dot segfaults on building one inheritance graph, leaving a 0-byte file
+badfile="doc/html/classHash_1_1hash__table__inherit__graph.png"
+if [ -f "$badfile" -a ! -s "$badfile" ] ; then
+ rm -f "$badfile"
+fi
+
+%check
+LD_LIBRARY_PATH=`pwd`/lib make regressonly4
+
+%post -p /sbin/ldconfig
+
+%postun -p /sbin/ldconfig
+
+%clean
+rm -rf %{buildroot}
+
+%files
+%defattr(-,root,root,-)
+%doc INSTALL LICENSE PEOPLE README VERSION
+%{_bindir}/cvc3
+%{_libdir}/libcvc3.so.*
+
+%files devel
+%defattr(-,root,root,-)
+%{_includedir}/cvc3
+%{_libdir}/*.so
+
+%files doc
+%defattr(-,root,root,-)
+%doc doc/html
+
+%files java
+%defattr(-,root,root,-)
+%{_libdir}/%{name}
+
+%files emacs
+%defattr(-,root,root,-)
+%{_datadir}/emacs/site-lisp/*.elc
+
+%files emacs-el
+%defattr(-,root,root,-)
+%{_datadir}/emacs/site-lisp/*.el
+
+%files xemacs
+%defattr(-,root,root,-)
+%{_datadir}/xemacs/site-packages/lisp/*.elc
+
+%files xemacs-el
+%defattr(-,root,root,-)
+%{_datadir}/xemacs/site-packages/lisp/*.el
+
+%changelog
+* Mon Oct 19 2009 Jerry James - 2.1-2
+- Fix problems found on review
+- Enable the Java interface
+
+* Thu Oct 15 2009 Jerry James - 2.1-1
+- Initial RPM
diff --git a/import.log b/import.log
new file mode 100644
index 0000000..36f4c1b
--- /dev/null
+++ b/import.log
@@ -0,0 +1 @@
+cvc3-2_1-2_fc11:HEAD:cvc3-2.1-2.fc11.src.rpm:1256228722
diff --git a/sources b/sources
index e69de29..07ae57c 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+d3756ab645f2e8d567217d8be16a4404 cvc3-2.1.tar.gz