From fe8034731d3f43fa9d0f8ebe5d72d085779752fe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Dec 2022 21:02:23 -0800
Subject: [PATCH] fix #6501

---
 src/ast/decl_collector.cpp        | 29 +++++++++++++++--------------
 src/smt/smt_context.cpp           |  4 ++++
 src/smt/smt_context.h             |  2 ++
 src/smt/theory_recfun.cpp         |  2 +-
 src/tactic/core/simplify_tactic.h | 17 +++++++++++++++++
 5 files changed, 39 insertions(+), 15 deletions(-)

diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
index 5b634abbd..7786a79d4 100644
--- a/src/ast/decl_collector.cpp
+++ b/src/ast/decl_collector.cpp
@@ -32,9 +32,8 @@ void decl_collector::visit_sort(sort * n) {
             m_todo.push_back(cnstr);
             ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
             unsigned num_cas = cnstr_acc.size();
-            for (unsigned j = 0; j < num_cas; j++) {
-                m_todo.push_back(cnstr_acc.get(j));
-            }
+            for (unsigned j = 0; j < num_cas; j++) 
+                m_todo.push_back(cnstr_acc.get(j));            
         }
     }
     for (unsigned i = n->get_num_parameters(); i-- > 0; ) {
@@ -49,14 +48,19 @@ bool decl_collector::is_bool(sort * s) {
 
 void decl_collector::visit_func(func_decl * n) {
     func_decl* g;
+
     if (!m_visited.is_marked(n)) {
         family_id fid = n->get_family_id();
         if (fid == null_family_id) 
             m_decls.push_back(n);
         else if (fid == m_rec_fid) {
-            m_rec_decls.push_back(n);
             recfun::util u(m());
-            m_todo.push_back(u.get_def(n).get_rhs());
+            if (u.has_def(n)) {
+                m_rec_decls.push_back(n);
+                m_todo.push_back(u.get_def(n).get_rhs());
+            }
+            else 
+                m_decls.push_back(n);            
         }
         else if (m_ar_util.is_as_array(n, g)) 
             m_todo.push_back(g);
@@ -97,13 +101,11 @@ void decl_collector::visit(ast* n) {
             case AST_QUANTIFIER: {
                 quantifier * q = to_quantifier(n);
                 unsigned num_decls = q->get_num_decls();
-                for (unsigned i = 0; i < num_decls; ++i) {
-                    m_todo.push_back(q->get_decl_sort(i));
-                }
+                for (unsigned i = 0; i < num_decls; ++i) 
+                    m_todo.push_back(q->get_decl_sort(i));                
                 m_todo.push_back(q->get_expr());
-                for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
-                    m_todo.push_back(q->get_pattern(i));
-                }
+                for (unsigned i = 0; i < q->get_num_patterns(); ++i) 
+                    m_todo.push_back(q->get_pattern(i));                
                 break;
             }
             case AST_SORT: 
@@ -111,9 +113,8 @@ void decl_collector::visit(ast* n) {
                 break;
             case AST_FUNC_DECL: {
                 func_decl * d = to_func_decl(n);
-                for (sort* srt : *d) {
-                    m_todo.push_back(srt);
-                }
+                for (sort* srt : *d) 
+                    m_todo.push_back(srt);                
                 m_todo.push_back(d->get_range());
                 visit_func(d);
                 break;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 45c469bde..d1cf2d875 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3027,6 +3027,10 @@ namespace smt {
         TRACE("end_assert_expr_ll", ast_mark m; m_asserted_formulas.display_ll(tout, m););
     }
 
+    void context::add_asserted(expr* e) {
+        m_asserted_formulas.assert_expr(e);
+    }
+
     void context::assert_expr(expr * e) {
         assert_expr(e, nullptr);
     }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 2b3a343f7..b6bf04a20 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1618,6 +1618,8 @@ namespace smt {
 
         void register_plugin(theory * th);
 
+        void add_asserted(expr* e);
+
         void assert_expr(expr * e);
 
         void assert_expr(expr * e, proof * pr);
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 515a51a17..6a8f2ab60 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -249,7 +249,7 @@ namespace smt {
             expr_ref eq1(m.mk_eq(l, r), m);
             expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
             expr_ref eq(m.mk_eq(fn, eq1), m);
-            ctx.assert_expr(eq);
+            ctx.add_asserted(eq);
             ctx.internalize_assertions();
             lit = mk_literal(fn);
         }
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index 39e3e9bde..1594b3d37 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/src/tactic/core/simplify_tactic.h
@@ -41,6 +41,23 @@ from two equivalent formulas are guaranteed to be equal.
   (apply simplify)
 ```
 
+The simplifier is also exposed as a stand-alone command.
+There are several options to control its behavior.
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(declare-fun p (Int) Bool)
+(assert (p (* (+ x y) (+ z u))))
+(apply simplify)
+(apply (with simplify :som true))
+
+(simplify (* (+ x y) (+ z u)) :som false)
+(simplify (* (+ x y) (+ z u)) :som true)
+```
+
 ### Notes
 
 * supports unsat cores, proof terms