diff --git a/src/tactic/ackr/ackr_helper.cpp b/src/tactic/ackr/ackr_helper.cpp
index b3a6a07d1..803fc3c54 100644
--- a/src/tactic/ackr/ackr_helper.cpp
+++ b/src/tactic/ackr/ackr_helper.cpp
@@ -16,7 +16,6 @@
 --*/
 #include"ackr_helper.h"
 
-
 double ackr_helper::calculate_lemma_bound(ackr_helper::fun2terms_map& occurrences) {
     fun2terms_map::iterator it = occurrences.begin();
     const fun2terms_map::iterator end = occurrences.end();
diff --git a/src/tactic/ackr/ackr_helper.h b/src/tactic/ackr/ackr_helper.h
index c89ebc09e..5c572907e 100644
--- a/src/tactic/ackr/ackr_helper.h
+++ b/src/tactic/ackr/ackr_helper.h
@@ -58,9 +58,10 @@ class ackr_helper {
         /** \brief Calculate n choose 2. **/
         inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
 
+        /** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/
         inline static double n_choose_2_chk(unsigned n) {
             SASSERT(std::numeric_limits<unsigned>().max() & 32);
-            return n & (1 << 16) ? n_choose_2(n) : std::numeric_limits<double>().infinity();;
+            return n & (1 << 16) ? std::numeric_limits<double>().infinity() : n_choose_2(n);
         }
     private:
         bv_util                              m_bvutil;