diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 6f4963990..732cbfc6f 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -85,7 +85,7 @@ namespace arith { m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); m_nla->settings().grobner_quota() = prms.arith_nl_gr_q(); m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency(); - m_nla->settings().expensive_patching() = prms.arith_nl_expp(); + m_nla->settings().expensive_patching() = false; } } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 65e51fe03..cf1d73892 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -292,7 +292,7 @@ class theory_lra::imp { m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); m_nla->settings().grobner_quota() = prms.arith_nl_gr_q(); m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency(); - m_nla->settings().expensive_patching() = prms.arith_nl_expp(); + m_nla->settings().expensive_patching() = false; } }