fix #5541

src/ast/ast_util.cpp

@@ -379,7 +379,7 @@ bool has_uninterpreted(ast_manager& m, expr* _e) {
     expr_ref e(_e, m);
     arith_util au(m);
     func_decl_ref f_out(m);
-    for (expr* arg : subterms(e)) {
+    for (expr* arg : subterms::all(e)) {
         if (!is_app(arg)) 
             continue;
         app* a = to_app(arg);

src/ast/for_each_expr.cpp

@@ -64,11 +64,11 @@ bool has_skolem_functions(expr * n) {
     return false;
 }
 
-subterms::subterms(expr_ref_vector const& es): m_es(es) {}
+subterms::subterms(expr_ref_vector const& es, bool include_bound): m_include_bound(include_bound), m_es(es) {}
-subterms::subterms(expr_ref const& e) : m_es(e.m()) { m_es.push_back(e); }
+subterms::subterms(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) { m_es.push_back(e); }
 subterms::iterator subterms::begin() { return iterator(*this, true); }
 subterms::iterator subterms::end() { return iterator(*this, false); }
-subterms::iterator::iterator(subterms& f, bool start): m_es(f.m_es) {
+subterms::iterator::iterator(subterms& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) {
     if (!start) m_es.reset();
 }
 expr* subterms::iterator::operator*() {
@@ -82,14 +82,15 @@ subterms::iterator subterms::iterator::operator++(int) {
 subterms::iterator& subterms::iterator::operator++() {
     expr* e = m_es.back();
     m_visited.mark(e, true);
-    if (is_app(e)) {
+    if (is_app(e)) 
-        for (expr* arg : *to_app(e)) {
+        for (expr* arg : *to_app(e)) 
             m_es.push_back(arg);            
-        }
+    else if (is_quantifier(e) && m_include_bound)
-    }
+        m_es.push_back(to_quantifier(e)->get_expr());
-    while (!m_es.empty() && m_visited.is_marked(m_es.back())) {
+
+    while (!m_es.empty() && m_visited.is_marked(m_es.back())) 
         m_es.pop_back();
-    }
+    
     return *this;
 }
 

src/ast/for_each_expr.h

@@ -168,9 +168,13 @@ bool has_skolem_functions(expr * n);
 
 // pre-order traversal of subterms
 class subterms {
+    bool            m_include_bound = false;
     expr_ref_vector m_es;
+    subterms(expr_ref const& e, bool include_bound);
+    subterms(expr_ref_vector const& es, bool include_bound);
 public:
     class iterator {
+        bool            m_include_bound = false;
         expr_ref_vector m_es;
         expr_mark       m_visited;        
     public:
@@ -181,8 +185,12 @@ public:
         bool operator==(iterator const& other) const;
         bool operator!=(iterator const& other) const;
     };
-    subterms(expr_ref_vector const& es);
+
-    subterms(expr_ref const& e);
+
+    static subterms all(expr_ref const& e) { return subterms(e, true); }
+    static subterms ground(expr_ref const& e) { return subterms(e, false); }
+    static subterms all(expr_ref_vector const& e) { return subterms(e, true); }
+    static subterms ground(expr_ref_vector const& e) { return subterms(e, false); }
     iterator begin();
     iterator end();
 };

src/ast/recfun_decl_plugin.cpp

@@ -466,7 +466,7 @@ namespace recfun {
             obj_map<expr, ptr_vector<expr>> parents;
             expr_ref tmp(e, m());
             parents.insert(e, ptr_vector<expr>());
-            for (expr* t : subterms(tmp)) {
+            for (expr* t : subterms::ground(tmp)) {
                 if (is_app(t)) {
                     for (expr* arg : *to_app(t)) {
                         parents.insert_if_not_there(arg, ptr_vector<expr>()).push_back(t);        

src/ast/rewriter/value_sweep.cpp

@@ -124,14 +124,14 @@ void value_sweep::init(expr_ref_vector const& terms) {
     m_vars.reset();
     m_qhead = 0;
     m_vhead = 0;
-    for (expr* t : subterms(terms)) {
+    for (expr* t : subterms::ground(terms)) {
         m_parents.reserve(t->get_id() + 1);
         if (get_value(t)) 
             m_queue.push_back(t);
         else if (!is_reducible(t))
             m_vars.push_back(t);
     }
-    for (expr* t : subterms(terms)) {
+    for (expr* t : subterms::ground(terms)) {
         if (!is_app(t)) 
             continue;
         for (expr* arg : *to_app(t)) {

src/ast/static_features.cpp

@@ -406,7 +406,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
     }    
 
     if (stack_depth > m_max_stack_depth) {
-        for (expr* arg : subterms(expr_ref(e, m)))
+        for (expr* arg : subterms::ground(expr_ref(e, m)))
             if (get_depth(arg) <= 3 || is_quantifier(arg)) 
                 process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10);
         return;

src/qe/qe_mbi.cpp

@@ -246,7 +246,7 @@ namespace qe {
         app_ref_vector avars(m); 
         bool_vector seen;
         arith_util a(m);
-        for (expr* e : subterms(lits)) {
+        for (expr* e : subterms::ground(lits)) {
             if ((m.is_eq(e) && a.is_int_real(to_app(e)->get_arg(0))) || a.is_arith_expr(e)) {
                 for (expr* arg : *to_app(e)) {
                     unsigned id = arg->get_id();
@@ -368,7 +368,7 @@ namespace qe {
     void uflia_mbi::add_arith_dcert(model& mdl, expr_ref_vector& lits) {
         obj_map<func_decl, ptr_vector<app>> apps;
         arith_util a(m);
-        for (expr* e : subterms(lits)) {
+        for (expr* e : subterms::ground(lits)) {
             if (a.is_int_real(e) && is_uninterp(e) && to_app(e)->get_num_args() > 0) {
                 func_decl* f = to_app(e)->get_decl();
                 apps.insert_if_not_there(f, ptr_vector<app>()).push_back(to_app(e));

src/sat/smt/q_mbi.cpp

@@ -448,7 +448,7 @@ namespace q {
     */
     void mbqi::extract_var_args(expr* _t, q_body& qb) {
         expr_ref t(_t, m);
-        for (expr* s : subterms(t)) {
+        for (expr* s : subterms::ground(t)) {
             if (is_ground(s))
                 continue;
             if (is_uninterp(s) && to_app(s)->get_num_args() > 0) {

src/sat/smt/q_model_fixer.cpp

@@ -243,7 +243,7 @@ namespace q {
             auto* info = (*this)(q);
             quantifier* flat_q = info->get_flat_q();
             expr_ref body(flat_q->get_expr(), m);
-            for (expr* t : subterms(body))
+            for (expr* t : subterms::ground(body))
                 if (is_uninterp(t) && !to_app(t)->is_ground())
                     fns.insert(to_app(t)->get_decl());
         }

src/tactic/core/solve_eqs_tactic.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 #include "ast/pb_decl_plugin.h"
+#include "ast/recfun_decl_plugin.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/hoist_rewriter.h"
@@ -407,6 +408,9 @@ class solve_eqs_tactic : public tactic {
         }
 
         void insert_solution(goal const& g, unsigned idx, expr* f, app* var, expr* def, proof* pr) {
+
+            if (!is_safe(var))
+                return;
             m_vars.push_back(var);
             m_candidates.push_back(f);
             m_candidate_set.mark(f);
@@ -708,7 +712,20 @@ class solve_eqs_tactic : public tactic {
                 if (!pr1) pr1 = g.pr(idx); else pr1 = m().mk_modus_ponens(g.pr(idx), pr1);
                 g.update(idx, tmp2, pr1, g.dep(idx));
             }            
+        }
 
+        expr_mark m_unsafe_vars;        
+
+        void filter_unsafe_vars() {
+            m_unsafe_vars.reset();
+            recfun::util rec(m());
+            for (func_decl* f : rec.get_rec_funs()) 
+                for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m())))
+                    m_unsafe_vars.mark(term);            
+        }
+
+        bool is_safe(expr* f) {
+            return !m_unsafe_vars.is_marked(f);
         }
         
         void sort_vars() {
@@ -1020,6 +1037,8 @@ class solve_eqs_tactic : public tactic {
                 m_subst      = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
                 m_norm_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
                 unsigned rounds = 0;
+
+                filter_unsafe_vars();
                 while (rounds < 20) {
                     ++rounds;
                     if (!m_produce_proofs && m_context_solve && rounds < 3) {

src/tactic/fd_solver/smtfd_solver.cpp

@@ -619,7 +619,7 @@ namespace smtfd {
             return false;
         }
         else if (round < max_rounds) {
-            for (expr* t : subterms(core)) {
+            for (expr* t : subterms::ground(core)) {
                 for (theory_plugin* p : m_plugins) {
                     p->check_term(t, round);
                 }
@@ -863,7 +863,7 @@ namespace smtfd {
                 }
                 mdl->register_decl(fn, fi);
             }
-            for (expr* t : subterms(terms)) {
+            for (expr* t : subterms::ground(terms)) {
                 if (is_uninterp_const(t) && sort_covered(t->get_sort())) {
                     expr_ref val = model_value(t);
                     mdl->register_decl(to_app(t)->get_decl(), val);
@@ -1305,7 +1305,7 @@ namespace smtfd {
 
 
         void populate_model(model_ref& mdl, expr_ref_vector const& terms) override {
-            for (expr* t : subterms(terms)) {
+            for (expr* t : subterms::ground(terms)) {
                 if (is_uninterp_const(t) && m_autil.is_array(t)) {
                     mdl->register_decl(to_app(t)->get_decl(), model_value_core(t));
                 }
@@ -1317,7 +1317,7 @@ namespace smtfd {
         void global_check(expr_ref_vector const& core) override {  
             expr_mark seen;
             expr_ref_vector shared(m), sharedvals(m);
-            for (expr* t : subterms(core)) {
+            for (expr* t : subterms::ground(core)) {
                 if (!is_app(t)) continue;
                 app* a = to_app(t);
                 unsigned offset = 0;
@@ -1463,7 +1463,7 @@ namespace smtfd {
             
             if (r == l_true) {
                 expr_ref qq(q->get_expr(), m);
-                for (expr* t : subterms(qq)) {
+                for (expr* t : subterms::ground(qq)) {
                     init_term(t);
                 }
                 m_solver->get_model(mdl);
@@ -1558,10 +1558,10 @@ namespace smtfd {
         void init_val2term(expr_ref_vector const& fmls, expr_ref_vector const& core) {
             m_val2term_trail.reset();
             m_val2term.reset();
-            for (expr* t : subterms(core)) {
+            for (expr* t : subterms::ground(core)) {
                 init_term(t);
             }
-            for (expr* t : subterms(fmls)) {
+            for (expr* t : subterms::ground(fmls)) {
                 init_term(t);
             }
         }
@@ -1719,12 +1719,12 @@ namespace smtfd {
             m_context.reset(m_model);
             expr_ref_vector terms(core);
             terms.append(m_axioms);
-            for (expr* t : subterms(core)) {
+            for (expr* t : subterms::ground(core)) {
                 if (is_forall(t) || is_exists(t)) {
                     has_q = true;
                 }
             }
-            for (expr* t : subterms(terms)) {
+            for (expr* t : subterms::ground(terms)) {
                 if (!is_forall(t) && !is_exists(t) && (!m_context.term_covered(t) || !m_context.sort_covered(t->get_sort()))) {
                     is_decided = l_false;
                 }
@@ -1733,7 +1733,7 @@ namespace smtfd {
 
             TRACE("smtfd", 
                   tout << "axioms: " << m_axioms << "\n";
-                  for (expr* a : subterms(terms)) {
+                  for (expr* a : subterms::ground(terms)) {
                       expr_ref val0 = (*m_model)(a);
                       expr_ref val1 = (*m_model)(abs(a));
                       if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) {
@@ -1750,7 +1750,7 @@ namespace smtfd {
 
             DEBUG_CODE(
                 bool found_bad = false;
-                for (expr* a : subterms(core)) {
+                for (expr* a : subterms::ground(core)) {
                     expr_ref val0 = (*m_model)(a);
                     expr_ref val1 = (*m_model)(abs(a));
                     if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) {