mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

cosmetics

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-06 10:19:17 -08:00
parent 228ef48628
commit 158a3db330
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/util/lp/nla_solver.cpp
View file

@ -376,6 +376,7 @@ struct solver::imp {
m_lar_solver.print_constraint(p.second, out); m_lar_solver.print_constraint(p.second, out);
out << " "; out << " ";
} }
out << "\n";
return out; return out;
} }
@ -2857,7 +2858,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_lemma(lemma.back(), std::cout << "expl & lemma: "); nla.m_imp->print_lemma_and_expl(std::cout);
ineq i0(llc::EQ, lp::lar_term(), rational(0)); ineq i0(llc::EQ, lp::lar_term(), rational(0));
i0.m_term.add_var(lp_a); i0.m_term.add_var(lp_a);