diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 386fdd8a2..505302dc1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5376,7 +5376,10 @@ extern "C" {
 
     /**
        \brief Add a new formula \c a to the given goal.
-        Conjunctions are split into separate formulas.
+        The formula is split according to the following procedure that is applied
+        until a fixed-point:
+           Conjunctions are split into separate formulas.
+           Negations are distributed over disjunctions, resulting in separate formulas.
         If the goal is \c false, adding new formulas is a no-op.
         If the formula \c a is \c true, then nothing is added.
         If the formula \c a is \c false, then the entire goal is replaced by the formula \c false.
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index b14d2676c..a3cac9e2e 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -137,7 +137,8 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
 }
 
 void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) {
-    if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
+    expr* g = 0;
+    if (!m().is_and(f) && !(m().is_not(f, g) && m().is_or(g))) {
         if (!save_first) {
             push_back(f, 0, d);
         }
@@ -170,8 +171,8 @@ void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) {
                 todo.push_back(expr_pol(t->get_arg(i), false));
             }
         }
-        else if (m().is_not(curr)) {
-            todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
+        else if (m().is_not(curr, g)) {
+            todo.push_back(expr_pol(g, !pol));
         }
         else {
             if (!pol) {