def non_negative(start, idx1, idx2, symbol):
    """
    Returns SMT constrains about constants being non-negative
    """
    result = ""
    for i in range(start, idx1):
        for j in range(idx2):
            const_name = symbol + str(i) + "_" + str(j)
            result += "(>= " + const_name + " 0)\n"
    return result