micro tuning for #4192

src/smt/smt_context.h

@@ -735,6 +735,10 @@ namespace smt {
 
         bool ts_visit_children(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo);
 
+        svector<expr_bool_pair> ts_todo;
+        svector<int>      tcolors;
+        svector<int>      fcolors;
+
         void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);
 
         void assert_default(expr * n, proof * pr);

src/smt/smt_internalizer.cpp

@@ -126,10 +126,7 @@ namespace smt {
         if (!def_int) {
             ptr_buffer<expr> descendants;
             get_foreign_descendants(to_app(n), fid, descendants);
-            ptr_buffer<expr>::iterator it  = descendants.begin();
-            ptr_buffer<expr>::iterator end = descendants.end();
-            for (; it != end; ++it) {
-                expr * arg = *it;
+            for (expr * arg : descendants) {
                 ts_visit_child(arg, false, tcolors, fcolors, todo, visited);
             }
             return visited;
@@ -154,27 +151,27 @@ namespace smt {
     }
 
     void context::top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs) {
-        svector<expr_bool_pair> todo;
-        svector<int>      tcolors;
-        svector<int>      fcolors;
-        todo.push_back(expr_bool_pair(n, true));
-        while (!todo.empty()) {
-            expr_bool_pair & p = todo.back();
+        ts_todo.reset();
+        tcolors.reset();
+        fcolors.reset();
+        ts_todo.push_back(expr_bool_pair(n, true));
+        while (!ts_todo.empty()) {
+            expr_bool_pair & p = ts_todo.back();
             expr * curr        = p.first;
             bool   gate_ctx    = p.second;
             switch (get_color(tcolors, fcolors, curr, gate_ctx)) {
             case White:
                 set_color(tcolors, fcolors, curr, gate_ctx, Grey);
-                ts_visit_children(curr, gate_ctx, tcolors, fcolors, todo);
+                ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo);
                 break;
             case Grey:
-                SASSERT(ts_visit_children(curr, gate_ctx, tcolors, fcolors, todo));
+                SASSERT(ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo));
                 set_color(tcolors, fcolors, curr, gate_ctx, Black);
                 if (n != curr && !m.is_not(curr))
                     sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx));
                 break;
             case Black:
-                todo.pop_back();
+                ts_todo.pop_back();
                 break;
             default:
                 UNREACHABLE();
@@ -185,7 +182,7 @@ namespace smt {
 #define DEEP_EXPR_THRESHOLD 1024
 
     void context::internalize_deep(expr* n) {
-        if (::get_depth(n) > DEEP_EXPR_THRESHOLD) {
+        if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD) {
             // if the expression is deep, then execute topological sort to avoid
             // stack overflow.
             // a caveat is that theory internalizers do rely on recursive descent so

src/smt/theory_fpa.cpp

@@ -388,16 +388,15 @@ namespace smt {
         context & ctx = get_context();
 
         expr_ref res(m), t(m);
+        expr_ref_vector fmls(m);
         proof_ref t_pr(m);
-        res = m.mk_true();
 
-        expr_ref_vector::iterator it = m_converter.m_extra_assertions.begin();
-        expr_ref_vector::iterator end = m_converter.m_extra_assertions.end();
-        for (; it != end; it++) {
-            ctx.get_rewriter()(*it, t, t_pr);
-            res = m.mk_and(res, t);
+        for (expr* arg : m_converter.m_extra_assertions) {
+            ctx.get_rewriter()(arg, t, t_pr);
+            fmls.push_back(t);
         }
         m_converter.m_extra_assertions.reset();
+        res = m.mk_and(fmls);
 
         m_th_rw(res);