diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index d38324db9..da704bd0b 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -281,17 +281,28 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
     };
 
     expr_ref_vector args(m);
-    for (expr * arg : *e) {
-        for (expr * child : tree(arg)) {
-            if (is_subexpr_arg(child, arg)) {
-                simplify(child);
-            }
-        }
-        r = simplify(arg);
-        args.push_back(r);
-        if (!assert_expr(simplify(arg), !is_and)) {
-            r = is_and ? m.mk_false() : m.mk_true();
-            return r;
+    if (m_forward) {
+        for (expr * arg : *e) {
+#define _SIMP_ARG(arg)                                          \
+            for (expr * child : tree(arg)) {                    \
+                if (is_subexpr_arg(child, arg)) {               \
+                    simplify(child);                            \
+                }                                               \
+            }                                                   \
+            r = simplify(arg);                                  \
+            args.push_back(r);                                  \
+            if (!assert_expr(simplify(arg), !is_and)) {         \
+                r = is_and ? m.mk_false() : m.mk_true();        \
+                return r;                                       \
+            }                                                   
+            _SIMP_ARG(arg);
+        }                                                                  
+    }
+    else {        
+        for (unsigned i = e->get_num_args(); i > 0; ) {
+            --i;
+            expr* arg = e->get_arg(i);
+            _SIMP_ARG(arg);
         }
     }
     pop(scope_level() - old_lvl);
@@ -319,6 +330,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         change = false;
 
         // go forwards
+        m_forward = true;
         if (!init(g)) return;
         unsigned sz = g.size();
         for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
@@ -336,6 +348,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         pop(scope_level());
         
         // go backwards
+        m_forward = false;
         if (!init(g)) return;
         sz = g.size();
         for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 6e5833cdb..581d40cd0 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -96,6 +96,7 @@ private:
     unsigned             m_max_depth;
     ptr_vector<expr>     m_empty;
     obj_pair_map<expr, expr, bool> m_subexpr_cache;
+    bool                 m_forward;
 
     expr_ref simplify(expr* t);
     expr_ref simplify_ite(app * ite);
@@ -122,7 +123,7 @@ public:
         m(m), m_simplifier(s), m_params(p), 
         m_trail(m), m_args(m), 
         m_dominators(m), 
-        m_scope_level(0), m_depth(0), m_max_depth(1024) {}
+        m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
 
 
     virtual ~dom_simplify_tactic() {}