diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp
index cfe0908d6..451a2b3dc 100644
--- a/src/muz/spacer/spacer_sym_mux.cpp
+++ b/src/muz/spacer/spacer_sym_mux.cpp
@@ -144,10 +144,12 @@ public:
 
     bool get_subst(expr * s, expr * & t, proof * & t_pr)
     {
-        if (!is_app(s)) { return false; }
+        if (!is_app(s)) 
+            return false; 
         app * a = to_app(s);
         func_decl * sym = a->get_decl();
         if (!m_parent.has_index(sym, m_from_idx)) {
+            CTRACE("spacer", m_homogenous && m_parent.is_muxed(sym), tout << "not found " << mk_pp(a, m) << "\n");
             SASSERT(!m_homogenous || !m_parent.is_muxed(sym));
             return false;
         }
diff --git a/src/tactic/arith/pb2bv_tactic.h b/src/tactic/arith/pb2bv_tactic.h
index e23c54d83..b1c94a6ba 100644
--- a/src/tactic/arith/pb2bv_tactic.h
+++ b/src/tactic/arith/pb2bv_tactic.h
@@ -13,7 +13,32 @@ Author:
 
     Christoph (cwinter) 2012-02-15
 
-Notes:
+Tactic Documentation:
+
+## Tactic pb2bv
+
+### Short Description
+
+Convert pseudo-boolean constraints to bit-vectors
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(assert (<= 0 x))
+(assert (<= 0 y))
+(assert (<= 0 z))
+(assert (<= 0 u))
+(assert (<= x 1))
+(assert (<= y 1))
+(assert (<= z 1))
+(assert (<= u 1))
+(assert (>= (+ (* 3 x) (* 2 y) (* 2 z) (* 2 u)) 4))
+(apply pb2bv)
+```
 
 --*/
 #pragma once
diff --git a/src/tactic/arith/propagate_ineqs_tactic.h b/src/tactic/arith/propagate_ineqs_tactic.h
index 47806a341..6341bf281 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.h
+++ b/src/tactic/arith/propagate_ineqs_tactic.h
@@ -4,30 +4,49 @@ Copyright (c) 2012 Microsoft Corporation
 Module Name:
 
     propagate_ineqs_tactic.h
-
-Abstract:
-
-    This tactic performs the following tasks:
-
-     - Propagate bounds using the bound_propagator.
-     - Eliminate subsumed inequalities.  
-       For example:
-          x - y >= 3
-          can be replaced with true if we know that
-          x >= 3 and y <= 0
-            
-     - Convert inequalities of the form p <= k and p >= k into p = k,
-       where p is a polynomial and k is a constant.
-
-    This strategy assumes the input is in arith LHS mode.
-    This can be achieved by using option :arith-lhs true in the
-    simplifier.
      
 Author:
 
     Leonardo (leonardo) 2012-02-19
 
-Notes:
+Tactic Documentation:
+
+## Tactic propagate-ineqs
+
+### Short Description
+
+Propagate ineqs/bounds, remove subsumed inequalities
+
+### Long Description
+
+This tactic performs the following tasks:
+
+- Propagate bounds using the bound_propagator.
+- Eliminate subsumed inequalities.
+  - For example:
+    `x - y >= 3` can be replaced with true if we know that `x >= 3` and `y <= 0`
+
+ - Convert inequalities of the form `p <= k` and `p >= k` into `p = k`,
+   where `p` is a polynomial and `k` is a constant.
+
+This strategy assumes the input is in arith LHS mode.
+This can be achieved by using option :arith-lhs true in the simplifier.
+
+### Example
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(declare-const v Int)
+(declare-const w Int)
+(assert (>= x 3))
+(assert (<= y 0))
+(assert (>= (- x y) 3))
+(assert (>= (* u v w) 2))
+(assert (<= (* v u w) 2))
+(apply (and-then simplify propagate-ineqs))
+```
 
 --*/
 #pragma once
diff --git a/src/tactic/arith/purify_arith_tactic.h b/src/tactic/arith/purify_arith_tactic.h
index ef5f08b61..4f3aa847a 100644
--- a/src/tactic/arith/purify_arith_tactic.h
+++ b/src/tactic/arith/purify_arith_tactic.h
@@ -42,7 +42,28 @@ Author:
 
     Leonardo de Moura (leonardo) 2011-12-30.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic purify-arith
+
+### Short Description
+
+Eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.
+These operators can be replaced by introcing fresh variables and using multiplication and addition.
+
+### Example
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(declare-const v Int)
+(declare-const w Int)
+(assert (= (div x 3) y))
+(assert (= (mod z 4) u))
+(assert (> (mod v w) u))
+(apply purify-arith)
+```
 
 --*/
 #pragma once