Z3_ast_vectorからZ3_astの配列を作成中にSegフォールトが発生する

Question

基本的に、私は多くのexprのORをとることを望みました。私はこれらのベクターを作成し、ベクトルから配列を作成してZ3_mk_orを使用しました。しかしコードはseg faultを投げます。

expr x = c.bool_const("x"); 
expr y = c.bool_const("y"); 
expr z = c.bool_const("z");  
int s=0; 
int size; 
Z3_ast* args; 
Z3_ast_vector vec; 
while(s < 2) 
{ 
    Z3_ast_vector_push(c, vec, x); 
    Z3_ast_vector_push(c, vec, y); 
    Z3_ast_vector_push(c, vec, z); 
    std::cout << "size: " << Z3_ast_vector_size(c, vec) << "\n"; 
    size = Z3_ast_vector_size(c, vec); 
    args = new Z3_ast[size]; 
    for(int i=0; i<size; ++i) 
    { 
     args[i] = Z3_ast_vector_get(c, vec, i); 
    } 

    expr r = to_expr(c, Z3_mk_or(c, size, args)); 
    s++; 
    Z3_ast_vector_resize(c, vec, 0); 
} 

また、これは私の問題に近づく正しい方法です。または多くのboolのconstへのより簡単なAPIコールはありませんか？ Z3で提供施設に固執する方が良いので、私は利便性のためにこれを追加しますが、CのAPIからの関数の使用が発生しやすい非常に誤りである

inline expr or(expr_vector const& args) { 
    array<Z3_ast> _args(args); 
    Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr()); 
    args.check_error(); 
    return expr(args.ctx(), r); 
} 

++：

Answer 1

は、あなたの代わりに補助関数を試みることができます.h