public Expr bp_smt(Context ctx, a_expression bp, ArrayList<arrayModification> am, ArrayList<parameter> functionInputs) throws Z3Exception{
		// bp is the a_expression 
		// am is a list of array modification
		// functionInputs is declared const
		HashMap<String,Expr> symbolTable = new HashMap<String, Expr>();
		parameter p;
		for(int i=0; i<functionInputs.size(); i++){ // input type can be int, double, boolean, int[], double[]
			p = functionInputs.get(i);
			if(p.type.equals("int"))
        		symbolTable.put(p.name, ctx.MkConst(p.name,ctx.IntSort()));
        	else if(p.type.equals("double"))
        		symbolTable.put(p.name, ctx.MkConst(p.name,ctx.RealSort()));
        	else if(p.type.equals("boolean"))
        		symbolTable.put(p.name, ctx.MkConst(p.name,ctx.BoolSort()));
        	else if(p.type.equals("int_array"))
        		symbolTable.put(p.name, ctx.MkConst(p.name, ctx.MkArraySort(ctx.IntSort(), ctx.IntSort())));
        	else if(p.type.equals("double_array"))
        		symbolTable.put(p.name, ctx.MkConst(p.name, ctx.MkArraySort(ctx.IntSort(), ctx.RealSort())));
        	else
        		System.out.println("Does not support the input type!");
        	
		}
		
		if(am.size()>0){
			arrayModification x = null;
			for(int i =0; i<am.size(); i++){
				x = am.get(i);
				if(symbolTable.containsKey(x.a)){
					//symbolTable.put(x.a, x.to_smt(ctx, symbolTable));
				}
			}
		}
		
		//Expr ret = bp.to_smt(ctx, symbolTable);
		return null;
	}