mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	revert new solve-eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									3a37cfca30
								
							
						
					
					
						commit
						9ef78fcfa7
					
				
					 2 changed files with 2 additions and 2 deletions
				
			
		| 
						 | 
				
			
			@ -33,7 +33,7 @@ inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = param
 | 
			
		|||
    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs");
 | 
			
		||||
}
 | 
			
		||||
 | 
			
		||||
#if 1
 | 
			
		||||
#if 0
 | 
			
		||||
inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
 | 
			
		||||
    return mk_solve_eqs2_tactic(m, p);
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -24,7 +24,7 @@ class tactic;
 | 
			
		|||
 | 
			
		||||
tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref());
 | 
			
		||||
 | 
			
		||||
#if 0
 | 
			
		||||
#if 1
 | 
			
		||||
inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
 | 
			
		||||
    return mk_solve_eqs1_tactic(m, p);
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue