mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	remove left-over debug output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									6d836e7e2f
								
							
						
					
					
						commit
						86af723db7
					
				
					 1 changed files with 0 additions and 2 deletions
				
			
		| 
						 | 
					@ -3983,7 +3983,6 @@ namespace z3 {
 | 
				
			||||||
            scoped_cb _cb(p, cb);
 | 
					            scoped_cb _cb(p, cb);
 | 
				
			||||||
            expr value(p->ctx(), _value);
 | 
					            expr value(p->ctx(), _value);
 | 
				
			||||||
            expr var(p->ctx(), _var);
 | 
					            expr var(p->ctx(), _var);
 | 
				
			||||||
            std::cout << "Fixed " << cb << "\n";
 | 
					 | 
				
			||||||
            p->m_fixed_eh(var, value);
 | 
					            p->m_fixed_eh(var, value);
 | 
				
			||||||
        }
 | 
					        }
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -4151,7 +4150,6 @@ namespace z3 {
 | 
				
			||||||
            assert(cb);
 | 
					            assert(cb);
 | 
				
			||||||
            expr conseq = ctx().bool_val(false);
 | 
					            expr conseq = ctx().bool_val(false);
 | 
				
			||||||
            array<Z3_ast> _fixed(fixed);
 | 
					            array<Z3_ast> _fixed(fixed);
 | 
				
			||||||
            std::cout << "conflict " << cb << " " << fixed << "\n";
 | 
					 | 
				
			||||||
            Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
 | 
					            Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
 | 
				
			||||||
        }
 | 
					        }
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue