mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-05 21:12:43 +00:00
Code Activity

fix the build and extend options to run grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-25 17:05:50 -08:00
parent 1d217595c8
commit aafdab65bd
5 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -1282,7 +1282,7 @@ lbool core::inner_check(bool constraint_derived) {
if (constraint_derived) {
if (need_to_call_algebraic_methods())
if (!(m_nla_settings.run_horner() && m_horner.horner_lemmas())) {
if (m_nla_settings.run_grobner())
if (m_nla_settings.run_grobner() == nla_settings::NEX_GROBNER || m_nla_settings.run_grobner() == nla_settings::BOTH_GROBNER)
m_grobner.grobner_lemmas();
}
if (done()) {