mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

regression failures fixes

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-06-29 09:57:29 -07:00
parent 4641d5f32d
commit d80f6e3222
2 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_lra.cpp
View file

@ -519,10 +519,10 @@ class theory_lra::imp {
while (!todo.empty()) {
expr* n = todo.back();
todo.pop_back();
expr* n1, *n2;
if (a.is_mul(n, n1, n2)) {
todo.push_back(n1);
todo.push_back(n2);
if (a.is_mul(n)) {
for (expr* arg : *to_app(n)) {
todo.push_back(arg);
}
}
else if (a.is_numeral(n, r1)) {
r *= r1;
@ -534,7 +534,7 @@ class theory_lra::imp {
vars.push_back(get_var_index(mk_var(n)));
}
}
TRACE("arith", tout << mk_pp(t, m) << "\n";);
TRACE("arith", tout << mk_pp(t, m) << " " << _has_var << "\n";);
if (!_has_var) {
ensure_nra();
m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
@ -862,6 +862,9 @@ public:
if (ctx().e_internalized(term) && th.is_attached_to_var(ctx().get_enode(term))) {
// skip
}
else if (a.is_numeral(term)) {
mk_enode(term);
}
else {
internalize_def(term);
}

2
src/util/lp/nra_solver.cpp
View file

@ -105,7 +105,7 @@ namespace nra {
// TBD: add variable bounds?
lbool r = m_nlsat->check();
TRACE("arith", m_nlsat->display(tout << r << "\n"););
TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
switch (r) {
case l_true:
break;