char cplex_version[] = "\nCPLEX 4.0 (19971111)\n";
char cplex_bsname[] = "CPLEX 4.0";