mirror of
				https://github.com/Z3Prover/z3
				synced 2025-10-31 11:42:28 +00:00 
			
		
		
		
	fix #1607 by filtering exceptions when the context is canceled
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									6bff15e12e
								
							
						
					
					
						commit
						6e03c7a542
					
				
					 2 changed files with 6 additions and 2 deletions
				
			
		|  | @ -139,7 +139,9 @@ extern "C" { | |||
|                 r = to_optimize_ptr(o)->optimize(); | ||||
|             } | ||||
|             catch (z3_exception& ex) { | ||||
|                 mk_c(c)->handle_exception(ex); | ||||
|                 if (!mk_c(c)->m().canceled()) { | ||||
|                     mk_c(c)->handle_exception(ex); | ||||
|                 } | ||||
|                 r = l_undef; | ||||
|             } | ||||
|             // to_optimize_ref(d).cleanup();
 | ||||
|  |  | |||
|  | @ -361,7 +361,9 @@ extern "C" { | |||
|             } | ||||
|             catch (z3_exception & ex) { | ||||
|                 to_solver_ref(s)->set_reason_unknown(eh); | ||||
|                 mk_c(c)->handle_exception(ex); | ||||
|                 if (!mk_c(c)->m().canceled()) { | ||||
|                     mk_c(c)->handle_exception(ex); | ||||
|                 } | ||||
|                 return Z3_L_UNDEF; | ||||
|             } | ||||
|         } | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue