diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 4411ed3d2..0c4983eec 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -107,7 +107,7 @@ class array_decl_plugin : public decl_plugin {
     func_decl * mk_set_subset(unsigned arity, sort * const * domain);
 
     func_decl * mk_as_array(func_decl * f);
-    
+
     func_decl * mk_choice(unsigned arity, sort* const* domain);
 
     bool is_array_sort(sort* s) const;
@@ -327,4 +327,3 @@ public:
 
 };
 
-
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 6ae84ebf4..91feac810 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -618,9 +618,9 @@ namespace smt {
         expr_ref px(mk_select(2, args1), m);
         expr* args2[2] = { pred, choice_term };
         expr_ref pc(mk_select(2, args2), m);
-        expr_ref ax(m.mk_implies(px, pc), m);
+        expr_ref body(m.mk_implies(px, pc), m);
         symbol x_name("x");
-        expr_ref q(m.mk_forall(1, &x_sort, &x_name, ax), m);
+        expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m);
         ctx.get_rewriter()(q);
         TRACE(array, tout << "choice " << q << "\n");        
         ctx.assert_expr(q);