diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 4411ed3d2e..092b457d8a 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;
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 736e447d32..7834dae900 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -619,12 +619,11 @@ 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);
-        literal l = mk_literal(q);
-        assert_axiom(l);
+        assert_axiom(mk_literal(q));
         return true;
     }