From 25112e47b46691ef0007068858cae034b9d72055 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 5 Jan 2023 20:59:28 -0800
Subject: [PATCH] bugfix to flatten-clases simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/flatten_clauses.h |  2 +-
 src/tactic/arith/add_bounds_tactic.h  | 24 ++++++++++++++++++++++--
 src/tactic/arith/lia2pb_tactic.h      | 24 ++++++++++++++++++++----
 3 files changed, 43 insertions(+), 7 deletions(-)

diff --git a/src/ast/simplifiers/flatten_clauses.h b/src/ast/simplifiers/flatten_clauses.h
index ab02faca1ea..2d65fd76d79 100644
--- a/src/ast/simplifiers/flatten_clauses.h
+++ b/src/ast/simplifiers/flatten_clauses.h
@@ -92,7 +92,7 @@ class flatten_clauses : public dependent_expr_simplifier {
                 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;
diff --git a/src/tactic/arith/add_bounds_tactic.h b/src/tactic/arith/add_bounds_tactic.h
index 0d42d8e6113..b69128c3eb1 100644
--- a/src/tactic/arith/add_bounds_tactic.h
+++ b/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
diff --git a/src/tactic/arith/lia2pb_tactic.h b/src/tactic/arith/lia2pb_tactic.h
index 860b04d1cd3..cd9c40634ca 100644
--- a/src/tactic/arith/lia2pb_tactic.h
+++ b/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