mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Java API: final adjustments
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
		
							parent
							
								
									5790115e40
								
							
						
					
					
						commit
						92e7384bf5
					
				
					 2 changed files with 2 additions and 8 deletions
				
			
		| 
						 | 
				
			
			@ -39,13 +39,6 @@ public class Context extends IDisposable
 | 
			
		|||
        initContext();
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    private Context(long ctx, long refCount)
 | 
			
		||||
    {
 | 
			
		||||
        super();
 | 
			
		||||
        this.m_ctx = ctx;
 | 
			
		||||
        this.m_refCount = refCount;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    /**
 | 
			
		||||
     * Creates a new symbol using an integer. <remarks> Not all integers can be
 | 
			
		||||
     * passed to this function. The legal range of unsigned integers is 0 to
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -128,7 +128,8 @@ public class Sort extends AST
 | 
			
		|||
 | 
			
		||||
    static Sort create(Context ctx, long obj) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        switch (Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj)))
 | 
			
		||||
        Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
 | 
			
		||||
        switch (sk)
 | 
			
		||||
        {
 | 
			
		||||
        case Z3_ARRAY_SORT:
 | 
			
		||||
            return new ArraySort(ctx, obj);
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue