mk_lstring method

Z3_ast mk_lstring(
  1. Z3_context c,
  2. int len,
  3. Z3_string s
)

\brief Create a string constant out of the string that is passed in It takes the length of the string as well to take into account 0 characters. The string is treated as if it is unescaped so a sequence of characters \u{0} is treated as 5 characters and not the character 0.

def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING)))

Implementation

Z3_ast mk_lstring(
  Z3_context c,
  int len,
  Z3_string s,
) {
  return _mk_lstring(
    c,
    len,
    s,
  );
}