mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
fix division filter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2c4a9c2f5c
commit
03ca330926
|
@ -23,7 +23,6 @@ namespace nla {
|
||||||
return;
|
return;
|
||||||
if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(q))
|
if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(q))
|
||||||
return;
|
return;
|
||||||
verbose_stream() << q << " " << x << " " << y << " " << null_lpvar << "\n";
|
|
||||||
m_idivisions.push_back({q, x, y});
|
m_idivisions.push_back({q, x, y});
|
||||||
m_core.trail().push(push_back_vector(m_idivisions));
|
m_core.trail().push(push_back_vector(m_idivisions));
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue