mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity

work on seed_properties

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-28 16:29:12 -10:00
parent 6ecba78d98
commit 8f726c11e6
3 changed files with 189 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/nlsat_explain.cpp
View file

@ -748,7 +748,7 @@ namespace nlsat {
bool have_zero = false;
for (unsigned i = 0; i < num_factors; ++i) {
f = m_factors.get(i);
if (coeffs_are_zeroes_in_factor(f)) {
if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
have_zero = true;
break;
}