check; get_model; check вызывает segfault в Z3 C API

Question

Я пытаюсь использовать Z3 через API C и smtlib2 для инкрементного решения. К сожалению, у меня возникло нарушение сегментации, когда вы утверждаете какую-то простую формулу, проверяете ее, получаете ее модель, утверждаете что-то дополнительное, а затем проверяете снова. Это также происходит без утверждения чего-то нового, т. Е. При проверке, поиске модели и повторной проверке. Вот минимальный пример для воспроизведения ошибки:

#include<z3.h> 

int main() 
{ 
    Z3_config cfg = Z3_mk_config(); 
    Z3_context ctx = Z3_mk_context(cfg); 
    Z3_ast fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a() Int) (assert (= a 0))", 0, 0, 0, 0, 0, 0); 
    Z3_solver solver = Z3_mk_solver(ctx); 
    Z3_solver_assert(ctx, solver, fs); 
    Z3_solver_check(ctx, solver); 
    Z3_model m = Z3_solver_get_model(ctx, solver); 
    Z3_solver_check(ctx, solver); 
    Z3_del_config(cfg); 
    return 0; 
} 

Я попытался с двумя Z3 версии (4.3.1 на Mac 64 бит и 4.1 на Ubuntu 64 бит).

Я ценю любую помощь, подсказки или обходные пути - возможно, я просто использую API неправильно?

Большого спасибо,

Элизабет

Answer 1

Вот версия коды с помощью подсчета ссылок. Сбой при удалении счетчика ссылок.

void main() { 
    Z3_config cfg = Z3_mk_config(); 
    Z3_context ctx = Z3_mk_context(cfg); 
    Z3_ast fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a() Int) (assert (= a 0))", 0, 0, 0, 0, 0, 0); 
    Z3_inc_ref(ctx, fs); 
    Z3_solver solver = Z3_mk_solver(ctx); 
    Z3_solver_inc_ref(ctx, solver); 
    Z3_solver_assert(ctx, solver, fs); 
    Z3_solver_check(ctx, solver); 
    Z3_model m = Z3_solver_get_model(ctx, solver); 
    Z3_model_inc_ref(ctx, m); 
    Z3_solver_check(ctx, solver); 


    // work with model 

    Z3_solver_dec_ref(ctx, solver); 
    Z3_model_dec_ref(ctx, m); 
    Z3_dec_ref(ctx, fs); 
    Z3_del_config(cfg); 
} 

BTW. API C++ скрывает все детали подсчета ссылок. С ним гораздо удобнее работать.