mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Negate premise in lemma; fixes (or at least hides) the segfault

Browse source
This commit is contained in:
Jakob Rath 2022-12-23 17:15:04 +01:00
parent 19e44e4f57
commit 993996c8a5
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/saturation.cpp
View file

@ -1290,7 +1290,7 @@ namespace polysat {
auto bound = ceil((m.two_to_N() - y_val - b_val) / x_bound); auto bound = ceil((m.two_to_N() - y_val - b_val) / x_bound);
b = bound; b = bound;
m_lemma.reset(); m_lemma.reset();
m_lemma.insert_eval(b_bound); // -b <= b_val m_lemma.insert_eval(~b_bound); // -b <= b_val
// TODO m_lemma.insert_eval(s.ule(y, y - b)); // -2^N < y - b < 2^N // TODO m_lemma.insert_eval(s.ule(y, y - b)); // -2^N < y - b < 2^N
verbose_stream() << "XX: " << b_bound << " " << s.uge(-a, b) << "\n"; verbose_stream() << "XX: " << b_bound << " " << s.uge(-a, b) << "\n";
// //

2
src/math/polysat/solver.cpp
View file

@ -963,7 +963,7 @@ namespace polysat {
appraise_lemma(lemmas.back()); appraise_lemma(lemmas.back());
} }
SASSERT(best_score < lemma_score::max()); SASSERT(best_score < lemma_score::max());
SASSERT(best_lemma); VERIFY(best_lemma);
unsigned const jump_level = std::max(best_score.jump_level(), base_level()); unsigned const jump_level = std::max(best_score.jump_level(), base_level());
SASSERT(jump_level <= max_jump_level); SASSERT(jump_level <= max_jump_level);