bugfix to flatten-clases simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/simplifiers/flatten_clauses.h

@@ -92,7 +92,7 @@ public:
                 if (decomposed) {
                     expr* na = mk_not(m, a);
                     for (expr* arg : *to_app(b))
-                        m_fmls.add(dependent_expr(m, m.mk_or(na, arg), nullptr, de.dep()));
+                        m_fmls.add(dependent_expr(m, m.mk_or(na, mk_not(m, arg)), nullptr, de.dep()));
                     m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr, nullptr));
                     ++m_num_flat;
                     continue;

src/tactic/arith/add_bounds_tactic.h

@@ -7,13 +7,33 @@ Module Name:
 
 Abstract:
 
-    Tactic for bounding unbounded variables.
+    
 
 Author:
 
     Leonardo de Moura (leonardo) 2011-06-30.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic add-bounds
+
+### Short Description
+
+Tactic for bounding unbounded variables.
+
+### Long Description
+
+The tactic creates a stronger sub-goal by adding bounds to variables.
+The new goal may not be satisfiable even if the original goal is.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(assert (> (+ x y) 10))
+(apply add-bounds)
+```
 
 --*/
 #pragma once

src/tactic/arith/lia2pb_tactic.h

@@ -5,15 +5,31 @@ Module Name:
 
     lia2pb_tactic.h
 
-Abstract:
-
-    Reduce bounded LIA benchmark into 0-1 LIA benchmark.
 
 Author:
 
     Leonardo de Moura (leonardo) 2012-02-07.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic lia2pb
+
+### Short Description
+
+Reduce bounded LIA benchmark into 0-1 LIA benchmark.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(assert (<= 0 x))
+(assert (<= x 5))
+(assert (<= 0 y))
+(assert (<= y 5))
+(assert (>= (+ (* 2 x) y) 5))
+(apply lia2pb)
+```
 
 --*/
 #pragma once