From 580012e19f4d7ed2227684e03c8b7183fb91498a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Mar 2022 09:44:56 -0800 Subject: [PATCH] fix #5894 expp is not implemented. This is the second time a fuzz bug reports it. Instead of closing the bug, just disable code path as fuzzers are not considering the comment from previous bug. --- src/sat/smt/arith_internalize.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 6f496399054..732cbfc6fa9 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 65e51fe03c3..cf1d738929e 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; } }