mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
remove debug out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
db79346ef7
commit
273aff5ed6
|
@ -251,7 +251,6 @@ struct propagate_ineqs_tactic::imp {
|
||||||
a_var x = mk_linear_pol(lhs);
|
a_var x = mk_linear_pol(lhs);
|
||||||
mpq c_prime;
|
mpq c_prime;
|
||||||
nm.set(c_prime, c.to_mpq());
|
nm.set(c_prime, c.to_mpq());
|
||||||
verbose_stream() << mk_ismt2_pp(t, m) << " bound " << c << "\n";
|
|
||||||
if (k == EQ) {
|
if (k == EQ) {
|
||||||
SASSERT(!strict);
|
SASSERT(!strict);
|
||||||
bp.assert_lower(x, c_prime, false);
|
bp.assert_lower(x, c_prime, false);
|
||||||
|
|
Loading…
Reference in a new issue