* Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.).

* Remove sat_module.cpp, which was no longer used (was previously refactored?)

3 files changed, 3 insertions, 5 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 8cfdab5af..80b689b8c 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -100,7 +100,7 @@ void inline makeZero(Bits& bits, unsigned width) {
  * 
  * @param a first term to be added
  * @param b second term to be added
- * @param sum the sum 
+ * @param res the result
  * @param carry the carry-in bit 
  * 
  * @return the carry-out
diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h
index 826b61d4f..5b53678dd 100644
--- a/src/theory/bv/bitblast_strategies.h
+++ b/src/theory/bv/bitblast_strategies.h
@@ -41,7 +41,6 @@ typedef std::vector<Node>    Bits;
  * Default Atom Bitblasting strategies: 
  * 
  * @param node the atom to be bitblasted
- * @param markerLit the marker literal corresponding to the atom
  * @param bb the bitblaster
  */
 
@@ -68,9 +67,8 @@ Node SleBB(TNode node, Bitblaster* bb);
  * Default Term Bitblasting strategies
  * 
  * @param node the term to be bitblasted
+ * @param bits [output parameter] bits representing the new term 
  * @param bb the bitblaster in which the clauses are added
- * 
- * @return the bits representing the new term 
  */
 
 void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); 
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index c86f14398..eb5f3e155 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -170,7 +170,7 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
 /** 
  * Asserts the clauses corresponding to the atom to the Sat Solver
  * by turning on the marker literal (i.e. setting it to false)
- * @param node the atom to be aserted
+ * @param node the atom to be asserted
  * 
  */