assertion violation in model generation

[joe-hauns]

I experienced an assertion violation (Debug) /segfault (Release) when generating a model for uninterpreted sorts with using the c++ api.

TL;DR: Reproduce with

#include <iostream>
#include <z3++.h>

using namespace std;
using namespace z3;

int main() {
  context ctxt;
#if 1
  auto srt = ctxt.uninterpreted_sort(ctxt.int_symbol(1));
#else
  auto srt = ctxt.uninterpreted_sort("alpha");
#endif 
  solver slvr(ctxt);

  auto a = ctxt.constant("a", srt);
  auto b = ctxt.constant("b", srt);

  slvr.add(a == b);
  slvr.check();
  
  auto model = slvr.get_model(); // <- assertion violation here
                                 // File: /path/to/z3/src/util/symbol.h
                                 // Line: 97
                                 // !is_numerical()
  cout << "got model." << endl;
  cout << "serializing:" << endl;
  cout << model << endl;
}

The issue is that when generating new names for new domain elements for the uninterpreted sort it is assumed that sorts have string identifiers, in order to serialize the sort name. The c++ api allows for non-string identifiers though.

...
        /**
           \brief create an uninterpreted sort with the name given by the string or symbol.
         */
        sort uninterpreted_sort(char const* name);
        sort uninterpreted_sort(symbol const& name);
...

Tested this issue with master 6d427d9 in Debug build, and some older commit in Release mode.