diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp
index 58b626808..54bd727d6 100644
--- a/src/muz/base/hnf.cpp
+++ b/src/muz/base/hnf.cpp
@@ -112,6 +112,12 @@ public:
         expr* n1, *n2;
         while (is_forall(n)) n = to_quantifier(n)->get_expr();
         if (m.is_implies(n, n1, n2) && is_predicate(n2)) {
+            if (is_var(n1)) {
+                return true;
+            }
+            if (is_quantifier(n1)) {
+                return false;
+            }
             app* a1 = to_app(n1);
             if (m.is_and(a1)) {
                 for (unsigned i = 0; i < a1->get_num_args(); ++i) {