mirror of
				https://github.com/Z3Prover/z3
				synced 2025-10-31 03:32:28 +00:00 
			
		
		
		
	do not set use_nra_model to true
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
		
							parent
							
								
									cc957011f2
								
							
						
					
					
						commit
						5de0b8a87f
					
				
					 1 changed files with 1 additions and 1 deletions
				
			
		|  | @ -404,7 +404,7 @@ struct solver::imp { | |||
|             lemma |= inq; | ||||
|         } | ||||
|         IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); | ||||
|         m_nla_core.set_use_nra_model(true); | ||||
|         //m_nla_core.set_use_nra_model(true);
 | ||||
|         return l_false; | ||||
|     } | ||||
| 
 | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue