mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f79dccccfe
commit
6071797ba9
|
@ -385,7 +385,7 @@ namespace nlsat {
|
|||
// TODO: check if it is useful to cache results
|
||||
SASSERT(m_assignment.is_assigned(max_var(p)));
|
||||
int r = m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment);
|
||||
return r > 0 ? +1 : (r < 0 ? 0 : -1);
|
||||
return r > 0 ? +1 : (r < 0 ? -1 : 0);
|
||||
}
|
||||
|
||||
bool satisfied(int sign, atom::kind k) {
|
||||
|
|
|
@ -2102,10 +2102,7 @@ namespace nlsat {
|
|||
del_ill_formed_lemmas();
|
||||
TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout););
|
||||
reinit_cache();
|
||||
for (var x = 0; x < num_vars(); x++) {
|
||||
if (new_assignment.is_assigned(x))
|
||||
m_assignment.set(x, new_assignment.value(x));
|
||||
}
|
||||
m_assignment.swap(new_assignment);
|
||||
reattach_arith_clauses(m_clauses);
|
||||
reattach_arith_clauses(m_learned);
|
||||
TRACE("nlsat_reorder", tout << "solver after variable reorder\n"; display(tout); display_vars(tout););
|
||||
|
|
Loading…
Reference in a new issue