fix #6501

src/ast/decl_collector.cpp

@@ -32,11 +32,10 @@ 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++) {
+            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; ) {
         parameter const& p = n->get_parameter(i);
         if (p.is_ast()) m_todo.push_back(p.get_ast());
@@ -49,15 +48,20 @@ 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());
+            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);
         m_visited.mark(n, true);
@@ -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) {
+                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) {
+                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) {
+                for (sort* srt : *d) 
                     m_todo.push_back(srt);                
-                }
                 m_todo.push_back(d->get_range());
                 visit_func(d);
                 break;

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);
     }

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);

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);
         }

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