yices_term_to_string() does not escape illegal variable names

[daniel-raffler]

Hello,
we would like to use yices_term_to_string() to generate short SMTLIB scripts from yices terms. Unfortunately the function does not seem to escape illegal variable names, which can lead to broken output strings.

Here is an example:

#include <yices.h>

int main() {
  yices_init();
  type_t int_type = yices_int_type();
  term_t x = yices_new_uninterpreted_term(int_type);
  term_t y = yices_new_uninterpreted_term(int_type);
  yices_set_term_name(x, "x");
  yices_set_term_name(y, ")");
  term_t formula = yices_arith_eq_atom(x, y);
  char* output = yices_term_to_string(formula, 1000, 1, 0);
  printf("%s\n", output);
  yices_exit();
  return 0;
}

Running this program will print (= x )) to the console. This is not a valid formula and trying to read it back in with yices_parse_term will result in a segmentation fault. In the SMTLIB format the problem is solved by quoting such variable names with |s. The output then becomes (= x |)|) for our example. (Other than parentheses there are some more restrictions on what may be included as part of a variable name. A full definition can be found on page 23 of the SMTLIB standard (link) under "Symbols".)

Would it be possible to add SMTLIB quoting to yices?