mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									8c085f1a18
								
							
						
					
					
						commit
						5b57c6b780
					
				
					 1 changed files with 1 additions and 1 deletions
				
			
		| 
						 | 
				
			
			@ -69,7 +69,6 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
 | 
			
		|||
        turn = !turn;
 | 
			
		||||
        (*preds)[turn].reset();
 | 
			
		||||
        reset(m_uf0);
 | 
			
		||||
        unsigned v1 = 0, v2 = 0;
 | 
			
		||||
        VERIFY(is_and(es[j], args[turn]));
 | 
			
		||||
 | 
			
		||||
        for (expr* e : *args[turn]) {
 | 
			
		||||
| 
						 | 
				
			
			@ -196,6 +195,7 @@ bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
 | 
			
		|||
void hoist_rewriter::reset(basic_union_find& uf) {
 | 
			
		||||
    uf.reset();
 | 
			
		||||
    for (expr* e : m_var2expr) {
 | 
			
		||||
        (void)e;
 | 
			
		||||
        uf.mk_var();
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue