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.
Z3Prover · Mar 10, 2022 · 580012e · 580012e
1 parent f26c12a
commit 580012e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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;
         }
     }