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

fix #3298

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-15 10:14:26 -07:00 • committed by Lev Nachmanson
parent d3a7ebee02
commit e7960e63da
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/emonics.cpp
View file

@ -448,6 +448,10 @@ std::ostream& emonics::display(std::ostream& out) const {
} }
display_use(out); display_use(out);
//display_uf(out); //display_uf(out);
out << "table:\n";
for (auto const& k : m_cg_table) {
out << k << "\n";
}
return out; return out;
} }
@ -543,6 +547,7 @@ bool emonics::invariant() const {
}; };
unsigned idx = 0; unsigned idx = 0;
for (auto const& m : m_monics) { for (auto const& m : m_monics) {
CTRACE("nla_solver_mons", !m_cg_table.contains(m.var()), tout << "removed " << m << "\n";);
SASSERT(m_cg_table.contains(m.var())); SASSERT(m_cg_table.contains(m.var()));
for (auto v : m.vars()) { for (auto v : m.vars()) {
if (!find_index(v, idx)) if (!find_index(v, idx))