mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix $4457
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d3e20d41b2
commit
3f2dafe047
|
@ -235,7 +235,6 @@ interval::interval(interval const & other):
|
|||
m_upper_open(other.m_upper_open),
|
||||
m_lower_dep(other.m_lower_dep),
|
||||
m_upper_dep(other.m_upper_dep) {
|
||||
std::cout << "copy " << m_lower << " " << m_upper << "\n";
|
||||
}
|
||||
|
||||
interval & interval::operator=(interval const & other) {
|
||||
|
|
|
@ -1995,7 +1995,6 @@ bool theory_arith<Ext>::is_inconsistent2(grobner::equation const * eq, grobner &
|
|||
grobner::monomial const * m = eq->get_monomial(i);
|
||||
intervals.push_back(mk_interval_for(m));
|
||||
}
|
||||
std::cout << intervals.size() << "\n";
|
||||
sbuffer<bool> deleted;
|
||||
deleted.resize(num, false);
|
||||
ptr_buffer<grobner::monomial> monomials;
|
||||
|
|
Loading…
Reference in a new issue