Minor fixes, spelling etc.

diff --git a/.mailmap b/.mailmap
index 1560f02723681210c6349b8ca00dad0f77200ca8..7cf2a12f010f09429bcfd067fbc06851b9569833 100644 (file)
--- a/.mailmap
+++ b/.mailmap
@@ -5,6 +5,8 @@ Dejan Jovanovic <dejan@cs.nyu.edu> <dejan.jovanovic@gmail.com>
 Francois Bobot <francois@bobot.eu> <francois@bobot.eu>
 Liana Hadarean <lianah@cs.nyu.edu> <lianahady@gmail.com>
 Andrew Reynolds <andrew.j.reynolds@gmail.com> <andrew.j.reynolds@gmail.com>
+Andrew Reynolds <andrew.j.reynolds@gmail.com> <reynolds@laraserver2.epfl.ch>
+Andrew Reynolds <andrew.j.reynolds@gmail.com> <reynolds@larapc05.epfl.ch>
 Cesare Tinelli <cesare-tinelli@uiowa.edu> <cesare-tinelli@uiowa.edu>
 Christopher L. Conway <christopherleeconway@gmail.com> <christopherleeconway@gmail.com>
 Clark Barrett <barrett@cs.nyu.edu> <barrett@cs.nyu.edu>

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 26ed8c296b82735c5ee12938ba2ee32513894d22..683f002cf8fb5f06e1041c2b42f89edc60e73bdc 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -105,7 +105,7 @@ private:
 
 
   /**
-   * Return the uinterpreted function symbol corresponding to division-by-zero
+   * Return the uninterpreted function symbol corresponding to division-by-zero
    * for this particular bit-width
    * @param k should be UREM or UDIV
    * @param width
@@ -121,7 +121,7 @@ private:
   NodeSet d_staticLearnCache;
   
   /**
-   * Maps from bit-vector width to divison-by-zero uninterpreted
+   * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
    */
   __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f8f1744edb81a62e97bf77c54ef1449e9a3a8ab1..1cdf5e8bdffb4c88c52bdd9052185d5bd09c032d 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -72,10 +72,10 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de
  when to apply instantiation
 option instMaxLevel --inst-max-level=N int :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
- 
+
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
- 
+
 option fullSaturateQuant --full-saturate-quant bool :default false
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 
@@ -105,7 +105,7 @@ option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :def
 option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
  only add one instantiation per quantifier per round for mbqi
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
- only add instantiations for one quantifier per round for mbqi 
+ only add instantiations for one quantifier per round for mbqi
 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 2462896c727e11fd6ab13e1765af998bcd83dbcd..a9d276f422fc787151523b87ffae7b50f47fe423 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -66,7 +66,7 @@ public:
     d_engine(engine) {
   }
 
-  /*
+  /**
    * Return true if n has an associated SAT literal
    */
   bool isSatLiteral(TNode n) const;