fix #4125

src/ast/normal_forms/nnf.cpp

@@ -142,7 +142,7 @@ class skolemizer {
                 }
             }
         }
-        r = s(body, substitution.size(), substitution.c_ptr());
+        r = s(body, substitution);
         p = nullptr;
         if (m_proofs_enabled) {
             if (q->get_kind() == forall_k) 

src/qe/qe.cpp

@@ -2464,6 +2464,27 @@ namespace qe {
         fml = tmp;
     }
 
+    bool has_quantified_uninterpreted(ast_manager& m, expr* fml) {
+        struct found {};
+        struct proc {
+            ast_manager& m;
+            proc(ast_manager& m):m(m) {}
+            void operator()(quantifier* q) {
+                if (has_uninterpreted(m, q->get_expr()))
+                    throw found();
+            }
+            void operator()(expr*) {}
+        };
+
+        try {
+            proc p(m);
+            for_each_expr(p, fml);
+            return false;
+        }
+        catch (found) {
+            return true;
+        }
+    }
     
     class simplify_solver_context : public i_solver_context {
         ast_manager&             m;

src/qe/qe.h

@@ -328,6 +328,8 @@ namespace qe {
 
     void mk_exists(unsigned num_vars, app* const* vars, expr_ref& fml);
 
+    bool has_quantified_uninterpreted(ast_manager& m, expr* fml);
+
     void get_nnf(expr_ref& fml, i_expr_pred& pred, i_nnf_atom& mk_atom, atom_set& pos, atom_set& neg); 
 
     class simplify_rewriter_cfg : public default_rewriter_cfg {

src/qe/qsat.cpp

@@ -740,6 +740,9 @@ namespace qe {
            \brief create a quantifier prefix formula.
         */
         void hoist(expr_ref& fml) {
+            if (has_quantified_uninterpreted(m, fml)) {
+                throw tactic_exception("formula contains uninterpreted functions");
+            }
             proof_ref pr(m);
             label_rewriter rw(m);
             rw.remove_labels(fml, pr);
@@ -770,9 +773,6 @@ namespace qe {
             while (!vars.empty());
             SASSERT(m_vars.back().empty()); 
             initialize_levels();
-            if (has_uninterpreted(m, fml))
-                throw tactic_exception("formula contains uninterpreted functions");
-
             TRACE("qe", tout << fml << "\n";);
         }
 
@@ -834,8 +834,8 @@ namespace qe {
             expr_ref_vector core1(m), core2(m), dels(m);
             TRACE("qe", tout << core.size() << "\n";);
             mus mus(get_kernel(level).s());
-            for (unsigned i = 0; i < core.size(); ++i) {
+            for (expr* arg : core) {
-                app* a = to_app(core[i].get());                
+                app* a = to_app(arg);
                 max_level lvl = m_pred_abs.compute_level(a);
                 if (lvl.max() + 2 <= level) {     
                     VERIFY(core1.size() == mus.add_soft(a));
@@ -1194,9 +1194,9 @@ namespace qe {
                 return true;
             }
             for (unsigned i = 0; i < m_avars.size(); ++i) {
-                contains_app cont(m, m_avars[i].get());
+                contains_app cont(m, m_avars.get(i));
                 if (cont(proj)) {
-                    TRACE("qe", tout << "Projection contains free variable: " << mk_pp(m_avars[i].get(), m) << "\n";);
+                    TRACE("qe", tout << "Projection contains free variable: " << mk_pp(m_avars.get(i), m) << "\n";);
                     return false;
                 }
             }

src/tactic/ufbv/ufbv_rewriter.cpp

@@ -34,7 +34,8 @@ ufbv_rewriter::ufbv_rewriter(ast_manager & m):
     m_new_args(m), 
     m_rewrite_todo(m),
     m_rewrite_cache(m),
-    m_new_exprs(m) {
+    m_new_exprs(m),
+    m_in_processed(m) {
     params_ref p;
     p.set_bool("elim_and", true);
     m_bsimp.updt_params(p);
@@ -304,9 +305,10 @@ bool ufbv_rewriter::rewrite_visit_children(app * a) {
             expr * v = e;
             if (m_rewrite_cache.contains(e)) {
                 expr_bool_pair const & ebp = m_rewrite_cache.get(e);
-                if (ebp.second)
+                if (ebp.second) {
                     v = ebp.first;
                 }
+            }
             for (unsigned i = sz; i-- > 0;) {
                 if (m_rewrite_todo[i] == v) {
                     recursive = true;
@@ -385,7 +387,8 @@ expr * ufbv_rewriter::rewrite(expr * n) {
                 if (rewrite1(f, m_new_args, np)) {
                     rewrite_cache(e, np, false);
                     // No pop.
-                } else {
+                } 
+                else {
                     if (all_untouched) {
                         rewrite_cache(e, actual, true);
                     }
@@ -398,7 +401,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
                         TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m) << "\nnew_args: \n";
                               tout << m_new_args << "\n";
                               tout << "=====>\n";
-                              tout << "na:\n " << mk_pp(na, m) << "\n";);
+                              tout << "na:\n " << na << "\n";);
                         rewrite_cache(e, na, true);
                     }
                     m_rewrite_todo.pop_back();
@@ -654,6 +657,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
         if (!is_demodulator(np, large, small)) {
             // insert n' into m_processed
             m_processed.insert(np);
+            m_in_processed.push_back(np);
             // update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx)
             add_back_idx_proc proc(m_back_idx, np);
             for_each_expr(proc, np);

src/tactic/ufbv/ufbv_rewriter.h

@@ -165,6 +165,7 @@ class ufbv_rewriter {
     demodulator2lhs_rhs m_demodulator2lhs_rhs;
     expr_ref_buffer     m_todo;
     obj_hashtable<expr> m_processed;
+    expr_ref_vector     m_in_processed;
     expr_ref_vector     m_new_args;
 
     expr_ref_buffer     m_rewrite_todo;