char cplex_version[] = "\nAMPL/CPLEX(19990421)\n";