public Expr array_length(Context ctx, HashMap<String, Expr> symbolTable) throws Z3Exception{
		Expr ret = null;
		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)){
			ret = ctx.MkConst((((a_string)this.a_inputs.get(0).leaf).s+"_lastIndex"), ctx.IntSort());
		}
			
		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)){
			ret = ctx.MkConst((((a_string)((a_expressionT)this.a_inputs.get(0).leaf).e.leaf).s+"_lastIndex"), ctx.IntSort());
		}
		else
			System.out.println("array not defined!");
		return ret;
	}