diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index f085ac5d6..61c671602 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -343,7 +343,7 @@ namespace lp {
             return out;
         }
 
-        bool m_has_non_integral_term = false;
+        bool m_some_terms_are_ignored = false;
         std_vector<mpq> m_sum_of_fixed;
         // we have to use m_var_register because of the fresh variables: otherwise they clash with the existing lar_solver column indices
         var_register m_var_register;
@@ -779,26 +779,29 @@ namespace lp {
         std_vector<variable_branch_stats> m_branch_stats;
         std_vector<branch> m_branch_stack;
         std_vector<constraint_index> m_explanation_of_branches;
-        bool term_has_big_number(const lar_term* t) const {
-            for (const auto& p : *t)
+        bool term_has_big_number(const lar_term& t) const {
+            for (const auto& p : t)
                 if (p.coeff().is_big())
                     return true;
             return false;
         }
+
+        bool ignore_big_nums() const { return lra.settings().dio_ignore_big_nums(); }
+        
         void add_term_callback(const lar_term* t) {
             unsigned j = t->j();
             TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;);
             if (!lra.column_is_int(j)) {
                 TRACE("dio", tout << "ignored a non-integral column" << std::endl;);
-                m_has_non_integral_term = true;
+                m_some_terms_are_ignored = true;
                 return;
             }
 
             CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;);
 
-            if (term_has_big_number(t)) {
+            if (ignore_big_nums() && term_has_big_number(*t)) {
                 TRACE("dio", tout << "term_has_big_number\n";);
-                m_has_non_integral_term = true;
+                m_some_terms_are_ignored = true;
                 return;
             }
             m_added_terms.push_back(t);
@@ -815,11 +818,12 @@ namespace lp {
         void update_column_bound_callback(unsigned j) {
             if (!lra.column_is_int(j))
                 return;
-            if (lra.column_has_term(j) && !term_has_big_number(&lra.get_term(j)))
+            if (lra.column_has_term(j) &&
+                ignore_big_nums() && !term_has_big_number(lra.get_term(j)))
                 m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term   
             if (!lra.column_is_fixed(j))
                 return;
-            if (lra.get_lower_bound(j).x.is_big())
+            if (ignore_big_nums() && lra.get_lower_bound(j).x.is_big())
                 return;
             TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout););
             m_changed_columns.insert(j);
@@ -1054,7 +1058,9 @@ namespace lp {
         void process_changed_columns(std_vector<unsigned> &f_vector) {
             find_changed_terms_and_more_changed_rows();
             for (unsigned j: m_changed_terms) {
-                SASSERT(!term_has_big_number(&lra.get_term(j)));
+                if (j >= lra.column_count())
+                    continue;
+                SASSERT(!ignore_big_nums() || !term_has_big_number(lra.get_term(j)));
                 m_terms_to_tighten.insert(j);
                 if (j < m_l_matrix.column_count()) {
                     for (const auto& cs : m_l_matrix.column(j)) {
@@ -1346,10 +1352,13 @@ namespace lp {
             unsigned best_var = UINT_MAX;
             size_t min_new_vars = std::numeric_limits<size_t>::max();
             unsigned num_candidates = 0;
-
+            std::vector<unsigned> to_remove;
             for (unsigned j : q.m_q) {
                 size_t new_vars = 0;
-                if (!m_espace.has(j)) continue;
+                if (!m_espace.has(j)) {
+                    to_remove.push_back(j);
+                    continue;
+                }
                 if (m_k2s.has_key(j)) {
                     unsigned ei = m_k2s[j]; // entry index for substitution
                     for (const auto& p : m_e_matrix.m_rows[ei])
@@ -1377,6 +1386,10 @@ namespace lp {
             if (best_var != UINT_MAX)
                 q.remove(best_var);
 
+            for (unsigned j: to_remove)
+                q.remove(j);
+            
+            
             return best_var;
         }
         
@@ -1544,8 +1557,9 @@ namespace lp {
 
         // We will have lar_t, and let j is lar_t.j(), the term column. 
         // In the m_espace we have lar_t. The result of open_ml((1*j)) is lar_t - (1, j).
-        // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j()) 
-        void init_substitutions(const lar_term& lar_t, protected_queue& q) {
+        // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j())
+        // return false iff seen a big number and dio_ignore_big_nums() is true
+        bool init_substitutions(const lar_term& lar_t, protected_queue& q) {
             m_espace.clear();
             m_c = mpq(0);
             m_lspace.clear();
@@ -1553,16 +1567,21 @@ namespace lp {
             SASSERT(get_extended_term_value(lar_t).is_zero());
             for (const auto& p : lar_t) {
                 if (is_fixed(p.j())) {
-                    m_c += p.coeff() * lia.lower_bound(p.j()).x;
+                    const mpq& b = lia.lower_bound(p.j()).x;
+                    if (ignore_big_nums() && b.is_big())
+                        return false;
+                    m_c += p.coeff() * b;
                 }
                 else {
                     unsigned lj = lar_solver_to_local(p.j());
+                    SASSERT(!p.coeff().is_big());
                     m_espace.add(p.coeff(), lj);;
                     if (can_substitute(lj))
                         q.push(lj);
                 }
             }
             SASSERT(subs_invariant(lar_t.j()));
+            return true;
         }
 
         unsigned lar_solver_to_local(unsigned j) const {
@@ -1584,8 +1603,6 @@ namespace lp {
         
         lia_move tighten_on_espace(unsigned j) {
             mpq g = gcd_of_coeffs(m_espace.m_data, true);
-            TRACE("dio", tout << "after process_q_with_S\nt:";  print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
-            
             if (g.is_one())
                 return lia_move::undef;
             if (g.is_zero()) {
@@ -1623,7 +1640,8 @@ namespace lp {
                       lra.print_column_info(p.var(), tout);
                   }
                 );
-            init_substitutions(lra.get_term(j), q);
+            if (!init_substitutions(lra.get_term(j), q))
+                return lia_move::undef;
          
             TRACE("dio", tout << "t:";
                   tout << "m_espace:";
@@ -2218,6 +2236,8 @@ namespace lp {
             for (unsigned k = 0; k < lra.terms().size(); k++) {
                 const lar_term* t = lra.terms()[k];
                 if (!lia.column_is_int(t->j())) continue;
+                if (ignore_big_nums() && term_has_big_number(*t))
+                    continue;
                 SASSERT(t->j() != UINT_MAX);
                 for (const auto& p : (*t).ext_coeffs()) {
                     unsigned j = p.var();
@@ -2288,7 +2308,6 @@ namespace lp {
     public:
         lia_move check() {
             lra.stats().m_dio_calls++;
-            std::cout << "check" << std::endl;
             TRACE("dio", tout << lra.stats().m_dio_calls << std::endl;);
             std_vector<unsigned> f_vector;
             lia_move ret;
@@ -2778,8 +2797,8 @@ namespace lp {
         // needed for the template bound_analyzer_on_row.h
         const lar_solver& lp() const { return lra; }
         lar_solver& lp() {return lra;}
-        bool has_non_integral_term() const {
-            return m_has_non_integral_term;
+        bool some_terms_are_ignored() const {
+            return m_some_terms_are_ignored;
         }
     };
     // Constructor definition
@@ -2798,8 +2817,8 @@ namespace lp {
         m_imp->explain(ex);
     }
 
-    bool dioph_eq::has_non_integral_term() const {
-        return m_imp->has_non_integral_term();
+    bool dioph_eq::some_terms_are_ignored() const {
+        return m_imp->some_terms_are_ignored();
     }
     
 
diff --git a/src/math/lp/dioph_eq.h b/src/math/lp/dioph_eq.h
index e266e7dd6..9adc04da7 100644
--- a/src/math/lp/dioph_eq.h
+++ b/src/math/lp/dioph_eq.h
@@ -30,6 +30,6 @@ namespace lp {
         ~dioph_eq();
         lia_move check();
         void explain(lp::explanation&);
-        bool has_non_integral_term() const;
+        bool some_terms_are_ignored() const;
     };
 }
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 3b48a0405..fed9fa21e 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -188,8 +188,7 @@ namespace lp {
 
         bool should_gomory_cut() {
             bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() ||
-                                      m_dio.has_non_integral_term();
-            std::cout << "should_gomory_cut:" << dio_allows_gomory << std::endl;
+                                      m_dio.some_terms_are_ignored();
             return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
         }
 
diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg
index 2057b3823..a2ef9328e 100644
--- a/src/math/lp/lp_params_helper.pyg
+++ b/src/math/lp/lp_params_helper.pyg
@@ -6,5 +6,6 @@ def_module_params(module_name='lp',
                           ('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
                           ('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
                           ('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
+                          ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
                          ))
                          
\ No newline at end of file
diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp
index e2f780ee1..2e3c464de 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -38,4 +38,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
     m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();
     m_dio_branching_period = lp_p.dio_branching_period();m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
+    m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums();
 }
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index ab90fee38..587e49e96 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -261,6 +261,8 @@ private:
     unsigned         m_dio_branching_period = 100; //  do branching rarely
     unsigned         m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening
     bool             m_dump_bound_lemmas = false;
+    bool             m_dio_ignore_big_nums = false;
+
 public:
     bool print_external_var_name() const { return m_print_external_var_name; }
     bool propagate_eqs() const { return m_propagate_eqs;}
@@ -272,6 +274,7 @@ public:
     bool dio_enable_gomory_cuts() const { return m_dio_eqs && m_dio_enable_gomory_cuts; }
     bool dio_enable_hnf_cuts() const { return m_dio_eqs && m_dio_enable_hnf_cuts; }
     unsigned dio_branching_period() const { return m_dio_branching_period; }
+    bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; }
     void set_random_seed(unsigned s) { m_rand.set_seed(s); }
     unsigned dio_report_branch_with_term_tigthening_period() const { return m_dio_report_branch_with_term_tigthening_period; }
     bool bound_progation() const {