mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	disable tweak to seq until there are cycles to test further
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									894c60bdf9
								
							
						
					
					
						commit
						f375016a11
					
				
					 1 changed files with 1 additions and 1 deletions
				
			
		| 
						 | 
				
			
			@ -2180,7 +2180,7 @@ void theory_seq::internalize_eq_eh(app * atom, bool_var v) {
 | 
			
		|||
}
 | 
			
		||||
 | 
			
		||||
bool theory_seq::internalize_atom(app* a, bool) {
 | 
			
		||||
#if 0
 | 
			
		||||
#if 1
 | 
			
		||||
    return internalize_term(a);
 | 
			
		||||
#else
 | 
			
		||||
    if (is_skolem(m_eq, a)) {
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue