mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Code Activity

refactor

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-15 11:47:34 -07:00
parent dfa87e68dc
commit e4f609715f
4 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_explain.cpp
View file

@ -52,8 +52,8 @@ namespace nlsat {
bool m_add_zero_disc;
bool m_cell_sample;
assignment const & sample() const { return m_solver.get_assignment(); }
assignment & sample() { return m_solver.get_assignment(); }
assignment const & sample() const { return m_solver.sample(); }
assignment & sample() { return m_solver.sample(); }
struct todo_set {
polynomial::cache & m_cache;
@ -514,7 +514,7 @@ namespace nlsat {
if (max_var(p) == max)
elim_vanishing(p); // eliminate vanishing coefficients of max
if (is_const(p) || max_var(p) < max) {
int s = sign(p, m_solver.get_assignment(), m_am);
int s = sign(p, m_solver.sample(), m_am);
if (!is_const(p)) {
SASSERT(max_var(p) != null_var);
SASSERT(max_var(p) < max);