diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index a658315e3..8be98edfb 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -609,7 +609,7 @@ namespace arith {
         else if (v != euf::null_theory_var) {
             rational r = get_value(v);
             TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
-            SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
+            SASSERT("integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m.limit().is_canceled()));
             if (a.is_int(o) && !r.is_int()) 
                 r = floor(r);
             value = a.mk_numeral(r, o->get_sort());
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 54a3d63d8..eef873afa 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -320,6 +320,8 @@ namespace euf {
     void solver::validate_model(model& mdl) {
         if (!m_unhandled_functions.empty())
             return;
+        if (get_config().m_arith_ignore_int)
+            return;
         for (auto* s : m_solvers)
             if (s && s->has_unhandled())
                 return;