diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index ce3eb5844..05f47ada7 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -456,6 +456,22 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp
     return false;
 }
 
+void bool_rewriter::push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits) {
+    expr* narg;
+    if (m().is_not(arg, narg)) {
+        if (!neg_lits.is_marked(narg)) {
+            neg_lits.mark(narg);
+            new_args.push_back(arg);
+        }
+    }
+    else { 
+        if (!pos_lits.is_marked(arg)) {
+            pos_lits.mark(arg);            
+            new_args.push_back(arg);
+        }
+    }
+}
+
 /**
    \brief Apply local context simplification at (OR args[0] ... args[num_args-1])
    Basic idea:
@@ -473,6 +489,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
     bool modified = false;
     bool forward  = true;
     unsigned rounds = 0;
+    expr* narg;
 
     while (true) {
         rounds++;
@@ -481,20 +498,13 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
             verbose_stream() << "rounds: " << rounds << "\n";
 #endif
 
-#define PUSH_NEW_ARG(ARG) {                     \
-    new_args.push_back(ARG);                    \
-    if (m().is_not(ARG))                        \
-        neg_lits.mark(to_app(ARG)->get_arg(0)); \
-    else                                        \
-        pos_lits.mark(ARG);                     \
-}
 
 #define PROCESS_ARG()                                                                           \
         {                                                                                       \
             expr * arg = args[i];                                                               \
-            if (m().is_not(arg) && m().is_or(to_app(arg)->get_arg(0)) &&                        \
-                simp_nested_not_or(to_app(to_app(arg)->get_arg(0))->get_num_args(),             \
-                                   to_app(to_app(arg)->get_arg(0))->get_args(),                 \
+            if (m().is_not(arg, narg) && m().is_or(narg) &&                                     \
+                simp_nested_not_or(to_app(narg)->get_num_args(),                                \
+                                   to_app(narg)->get_args(),                                    \
                                    neg_lits,                                                    \
                                    pos_lits,                                                    \
                                    new_arg)) {                                                  \
@@ -515,11 +525,11 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
                 unsigned sz = to_app(arg)->get_num_args();                                      \
                 for (unsigned j = 0; j < sz; j++) {                                             \
                     expr * arg_arg = to_app(arg)->get_arg(j);                                   \
-                    PUSH_NEW_ARG(arg_arg);                                                      \
+                    push_new_arg(arg_arg, new_args, neg_lits, pos_lits);                        \
                 }                                                                               \
             }                                                                                   \
             else {                                                                              \
-                PUSH_NEW_ARG(arg);                                                              \
+                push_new_arg(arg, new_args, neg_lits, pos_lits);                                \
             }                                                                                   \
         }
 
@@ -528,7 +538,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
         static unsigned counter = 0;
         counter++;
         if (counter % 10000 == 0)
-            verbose_stream() << "local-ctx-cost: " << m_local_ctx_cost << "\n";
+            verbose_stream() << "local-ctx-cost: " << m_local_ctx_cost << " " << num_args << "\n";
 #endif
 
         if (forward) {
diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h
index b309f8032..b1d2dec53 100644
--- a/src/ast/rewriter/bool_rewriter.h
+++ b/src/ast/rewriter/bool_rewriter.h
@@ -75,6 +75,8 @@ class bool_rewriter {
     bool local_ctx_simp(unsigned num_args, expr * const * args, expr_ref & result);
     br_status try_ite_value(app * ite, app * val, expr_ref & result);
 
+    void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
+
 public:
     bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); }
     ast_manager & m() const { return m_manager; }