Z3: Создание перечислимого типа с количеством элементов, известных динамически

Я пытаюсь создать перечисляемый тип данных в Z3, где количество элементов известно только во время выполнения. У меня это работает с Python API, но я пытаюсь сделать то же самое, используя C и C ++ API вместе. Ниже приводится программа.

#include<stdio.h>
#include<stdlib.h>
#include<string.h>
#include<stdarg.h>
#include<memory.h>
#include<z3++.h>
using namespace std;
using namespace z3;

expr get_expr(context &c,Z3_func_decl constant)//get expression from constant
{
func_decl temp=to_func_decl(c, constant);
return(to_expr(c, Z3_mk_app(c, temp, 0, 0)));
}

sort create_enum(context &c,char const *dtypename,int count,char const *prefix,Z3_func_decl consts[])
{
int i;
char itemname[10];
Z3_symbol *names=new Z3_symbol[count];
Z3_func_decl *testers=new Z3_func_decl[count];
for(i=0;i<count;i++)
{
sprintf(itemname,"%s%d",prefix,i);
names[i]=Z3_mk_string_symbol(c,itemname);
}
Z3_symbol enum_nm = Z3_mk_string_symbol(c,dtypename);
sort s = to_sort(c, Z3_mk_enumeration_sort(c, enum_nm, 3, names, consts, testers));
return(s);
}

int main()
{context c;

int count=3,i;
char itemname[10],prefix[]={"p"},dtypename[]={"phynodetype"};
Z3_func_decl *phynodeconsts=new Z3_func_decl[count];
sort phynodetype=create_enum(c,"phynodetype",count,"p",phynodeconsts);
func_decl g = function("g", phynodetype, phynodetype);
solver s(c);
expr tst1= get_expr(c,phynodeconsts[0])==g(get_expr(c,phynodeconsts[1]));
expr tst2= get_expr(c,phynodeconsts[1])==g(get_expr(c,phynodeconsts[0]));
cout<<tst1<<endl<<tst2<<endl;
s.add(tst1);
s.add(tst2);
s.add(implies(a,b>=5));
s.add(b<5);
cout<<s.check();
cout<<s.get_model();}

Я занимаюсь созданием функции create_enum, которая будет принимать имя
новый тип данных, который я хочу создать, количество элементов и префикс (например, если количество элементов равно 3, а префикс равен «p», элементы будут называться p0, p1, p2). Программа продолжает поднимать SIGSEGV, и в редких случаях, когда это не так, я получаю очень странные результаты. Я использовал много кода из следующего поста:

Как использовать перечисленные константы после вызова какой-то тактики в Z3?

Кто-нибудь может сказать, что идет не так? Некоторые связанные запросы: Есть ли способ создания перечисляемых типов данных с использованием API C ++? Кажется, что expr, func_decl и т. Д. Не имеют конструктора по умолчанию, и мне нужно создать массив exprs. Выход из использования malloc ()?