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<

+//! t<

 Theorem BitvectorTheoremProducer::leftShiftToConcat(const Expr& e) {

   if(CHECK_PROOFS) {

     // The kids must be constant expressions

@@ -1963,7 +1963,7 @@

   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);

 }

-//! t<

+//! t<

 Theorem BitvectorTheoremProducer::constWidthLeftShiftToConcat(const Expr& e) {

   if(CHECK_PROOFS) {

     // The kids must be constant expressions

@@ -1996,7 +1996,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, <sum of shifts of t>) -- 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<string>& reasons)

+bool TheoryCore::incomplete(std::vector<std::string>& reasons)

 {

   if(d_incomplete.size() > 0) {

     for(CDMap<string,bool>::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<string>& constructors,

-                              const vector<vector<string> >& selectors,

-                              const vector<vector<Expr> >& types)

+Expr TheoryDatatype::dataType(const std::string& name,

+                              const std::vector<std::string>& constructors,

+                              const std::vector<std::vector<std::string> >& selectors,

+                              const std::vector<std::vector<Expr> >& types)

 {

   vector<string> names;

   vector<vector<string> > 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<string>& names,

-                              const vector<vector<string> >& allConstructors,

-                              const vector<vector<vector<string> > >& allSelectors,

-                              const vector<vector<vector<Expr> > >& allTypes)

+Expr TheoryDatatype::dataType(const std::vector<std::string>& names,

+                              const std::vector<std::vector<std::string> >& allConstructors,

+                              const std::vector<std::vector<std::vector<std::string> > >& allSelectors,

+                              const std::vector<std::vector<std::vector<Expr> > >& allTypes)

 {

   vector<Expr> 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<Expr>& 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<ExprMap<vector<dynTrig>* >*>& trig_maps, const Theorem& thm, size_t univs_id){

+void TheoryQuant::setupTriggers(ExprMap<ExprMap<std::vector<dynTrig>* >*>& trig_maps, const Theorem& thm, size_t univs_id){

   //  static std::vector<Expr> 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<ExprMap<vector<dynTrig>*>*>& new_trigs,

+void TheoryQuant::matchListNew(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs,

 			       const CDList<Expr>& glist,

 			       size_t gbegin,

 			       size_t gend){

@@ -7984,7 +7984,7 @@

   d_lastEqsUpdatePos.set(d_eqsUpdate.size());

 }

-void TheoryQuant::synCheckSat(ExprMap<ExprMap<vector<dynTrig>* >* >&  new_trigs, bool fullEffort){

+void TheoryQuant::synCheckSat(ExprMap<ExprMap<std::vector<dynTrig>* >* >&  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<string>& fields,

-		     const vector<Type>& types)

+Type VCL::recordType(const std::vector<std::string>& fields,

+		     const std::vector<Type>& 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<string>& selectors, const vector<Expr>& types)

+Type VCL::dataType(const std::string& name,

+                   const std::string& constructor,

+                   const std::vector<std::string>& selectors,

+                   const std::vector<Expr>& types)

 {

   vector<string> constructors;

   constructors.push_back(constructor);

@@ -806,10 +807,10 @@

 }

-Type VCL::dataType(const string& name,

-                   const vector<string>& constructors,

-                   const vector<vector<string> >& selectors,

-                   const vector<vector<Expr> >& types)

+Type VCL::dataType(const std::string& name,

+                   const std::vector<std::string>& constructors,

+                   const std::vector<std::vector<std::string> >& selectors,

+                   const std::vector<std::vector<Expr> >& types)

 {

   Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);

   if(d_dump) {

@@ -819,11 +820,11 @@

 }

-void VCL::dataType(const vector<string>& names,

-                   const vector<vector<string> >& constructors,

-                   const vector<vector<vector<string> > >& selectors,

-                   const vector<vector<vector<Expr> > >& types,

-                   vector<Type>& returnTypes)

+void VCL::dataType(const std::vector<std::string>& names,

+                   const std::vector<std::vector<std::string> >& constructors,

+                   const std::vector<std::vector<std::vector<std::string> > >& selectors,

+                   const std::vector<std::vector<std::vector<Expr> > >& types,

+                   std::vector<Type>& returnTypes)

 {

   Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);

   if(d_dump) {

@@ -1405,8 +1406,8 @@

 }

-Expr VCL::recordExpr(const vector<string>& fields,

-		     const vector<Expr>& exprs)

+Expr VCL::recordExpr(const std::vector<std::string>& fields,

+		     const std::vector<Expr>& exprs)

 {

   DebugAssert(fields.size() > 0, "VCL::recordExpr()");

   DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");

@@ -2107,7 +2108,7 @@

 }

-bool VCL::incomplete(vector<string>& reasons) {

+bool VCL::incomplete(std::vector<std::string>& reasons) {

   // TODO: add to interactive interface

   // Return true only after a failed query

   return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));