mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

remove output from normalize bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 17:46:53 -07:00
parent e2cab00b1b
commit f21b60a6e1
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/arith/normalize_bounds_tactic.cpp
View file

@ -124,9 +124,6 @@ class normalize_bounds_tactic : public tactic {
expr * curr = in->form(idx);
proof_ref new_pr(m);
m_rw(curr, new_curr, new_pr);
std::cout << new_curr << "\n";
std::cout << new_pr << "\n";
std::cout << expr_ref(in->pr(idx), m) << "\n";
if (produce_proofs) {
proof * pr = in->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);