public BoolExpr add_partitioned_theorem(Context ctx, HashMap<String, Expr> symbolTable) throws Z3Exception{
		// a, l1, u1, l2, u2
		Expr a = this.a_inputs.get(0).to_smt(ctx, symbolTable );
		Expr l1 = this.a_inputs.get(1).to_smt(ctx, symbolTable );
		Expr u1 = this.a_inputs.get(2).to_smt(ctx, symbolTable );
		Expr l2 = this.a_inputs.get(3).to_smt(ctx, symbolTable );
		Expr u2 = this.a_inputs.get(4).to_smt(ctx, symbolTable );
		
		
		String array_name="";
		if(this.a_inputs.get(0).leaf!=null && this.a_inputs.get(0).leaf.type.equals("string") && symbolTable.containsKey(((a_string)this.a_inputs.get(0).leaf).s))
			array_name = ((a_string)this.a_inputs.get(0).leaf).s;
		else if (this.a_inputs.get(0).leaf!=null && this.a_inputs.get(0).leaf.type.equals("a_expression") &&
				((a_expressionT)this.a_inputs.get(0).leaf).e.leaf!=null && ((a_expressionT)this.a_inputs.get(0).leaf).e.leaf.type.equals("string")
				&& symbolTable.containsKey(((a_string)((a_expressionT)this.a_inputs.get(0).leaf).e.leaf).s))
			array_name = ((a_string)((a_expressionT)this.a_inputs.get(0).leaf).e.leaf).s;
		else
			System.out.println("array not defined!");
		
		Expr alength = ctx.MkConst(array_name + "_lastIndex", ctx.IntSort());
        Expr i = ctx.MkConst(array_name+"_i", ctx.IntSort());
        Expr j = ctx.MkConst(array_name+"_j", ctx.IntSort());
        //ctx.MkLe(ctx.MkInt(-1), (ArithExpr)l1), ctx.MkLe((ArithExpr)u2, (ArithExpr) alength)
        BoolExpr instance_bound = ctx.MkAnd( new BoolExpr[]{ 
				ctx.MkLe((ArithExpr)l1, (ArithExpr)u1), ctx.MkLt((ArithExpr)u1, (ArithExpr)l2), 
				ctx.MkLe((ArithExpr)l2, (ArithExpr)u2)});
        
        BoolExpr partitioned_expr1 = ctx.MkAnd(new BoolExpr[]{ctx.MkLe((ArithExpr)l1, (ArithExpr) i), ctx.MkLe((ArithExpr) i, (ArithExpr) u1),
        												  ctx.MkLe((ArithExpr)l2, (ArithExpr) j), ctx.MkLe((ArithExpr) j, (ArithExpr)u2),
        												  ctx.MkLt((ArithExpr)i, (ArithExpr)j)});
        //BoolExpr partitioned_expr = ctx.MkAnd(new BoolExpr[]{ partitioned_expr1, ctx.MkLe((ArithExpr)ctx.MkSelect((ArrayExpr)a, i), (ArithExpr)ctx.MkSelect((ArrayExpr)a, j))});
        BoolExpr partitioned_expr = ctx.MkImplies(partitioned_expr1, ctx.MkLe((ArithExpr)ctx.MkSelect((ArrayExpr)a, i), (ArithExpr)ctx.MkSelect((ArrayExpr)a, j)));
        
        
        BoolExpr  partitioned= ctx.MkForall(new Expr[]{i, j}, /* names of quantified variables */
        		partitioned_expr, 1, null, null, null, null);
        
        return ctx.MkImplies(instance_bound,partitioned);
	}