diff --git a/lib/pdr_farkas_learner.cpp b/lib/pdr_farkas_learner.cpp
index 4cb441cbd..a9a6956c3 100644
--- a/lib/pdr_farkas_learner.cpp
+++ b/lib/pdr_farkas_learner.cpp
@@ -60,6 +60,11 @@ namespace pdr {
             return a.mk_add(e1, e2);
         }
 
+        app* mk_mul(expr* e1, expr* e2) {
+            mk_coerce(e1, e2);
+            return a.mk_mul(e1, e2);
+        }
+
         app* mk_le(expr* e1, expr* e2) {
             mk_coerce(e1, e2);
             return a.mk_le(e1, e2);
@@ -86,7 +91,7 @@ namespace pdr {
                 tmp = e;
             }
             else {
-                tmp = a.mk_mul(a.mk_numeral(c, a.is_int(e)), e);
+                tmp = mk_mul(a.mk_numeral(c, c.is_int() && a.is_int(e)), e);
             }
             res = mk_add(res, tmp);
         }
diff --git a/lib/theory_arith_core.h b/lib/theory_arith_core.h
index 6ca5b888e..a691096ec 100644
--- a/lib/theory_arith_core.h
+++ b/lib/theory_arith_core.h
@@ -479,8 +479,8 @@ namespace smt {
             return;
         }
         expr* to_r = m_util.mk_to_real(n);
-        expr* lo = m_util.mk_le(to_r, x);
-        expr* hi = m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false)));
+        expr_ref lo(m_util.mk_le(to_r, x), m);
+        expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m);
         mk_axiom(m.mk_false(), lo);
         mk_axiom(m.mk_false(), hi);
     }