diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index be3f80f92..ff49584ff 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -201,9 +201,15 @@ namespace eq {
             return (*m_is_variable)(e);
         }
         
-        bool is_neg_var(ast_manager & m, expr * e) {
+        bool is_neg_var(ast_manager & m, expr * e, var*& v) {
             expr* e1;
-            return m.is_not(e, e1) && is_variable(e1);
+            if (m.is_not(e, e1) && is_variable(e1)) {
+                v = to_var(e1);
+                return true;
+            }
+            else {
+                return false;
+            }
         }
         
         
@@ -328,18 +334,19 @@ namespace eq {
         
         bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) {
             expr* lhs, *rhs;
+            var* v;
             
             // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases    
             if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) {
                 // (iff (not VAR) t) (iff t (not VAR)) cases
                 if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) {
-                    if (!is_neg_var(m, lhs)) {
+                    if (!is_neg_var(m, lhs, v)) {
                         std::swap(lhs, rhs);
                     }
-                    if (!is_neg_var(m, lhs)) {
+                    if (!is_neg_var(m, lhs, v)) {
                         return false;
                     }
-                    vs.push_back(to_var(lhs));
+                    vs.push_back(v);
                     ts.push_back(m.mk_not(rhs));
                     TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
                     return true;
@@ -378,9 +385,9 @@ namespace eq {
             }
             
             // VAR = false case
-            if (is_neg_var(m, e)) {
+            if (is_neg_var(m, e, v)) {
                 ts.push_back(m.mk_false());
-                vs.push_back(to_var(to_app(e)->get_arg(0)));
+                vs.push_back(v);
                 TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
                 return true;
             }