diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 412744360f3..3da706e677f 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1735,7 +1735,6 @@ namespace smt {
         m_util(m),
         m_arith_eq_solver(m),
         m_arith_eq_adapter(*this, m_util),
-        m_asserted_qhead(0),
         m_row_vars_top(0),
         m_to_patch(1024),
         m_blands_rule(false),
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 7b76960dd68..c9bc9f31abb 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -754,6 +754,7 @@ namespace smt {
         if (!(consts / gcds).is_int()) {
             TRACE("gcd_test", tout << "row failed the GCD test:\n"; display_row_info(tout, r););
             antecedents ante(*this);
+            m_stats.m_gcd_conflicts++;
             collect_fixed_var_justifications(r, ante);
             context & ctx         = get_context();
             ctx.set_conflict(
@@ -833,6 +834,7 @@ namespace smt {
         numeral u1 = floor(u/gcds);
         
         if (u1 < l1) {
+            m_stats.m_gcd_conflicts++;
             TRACE("gcd_test", tout << "row failed the extended GCD test:\n"; display_row_info(tout, r););
             collect_fixed_var_justifications(r, ante);
             context & ctx         = get_context();