check; get_model; check causes segfault in Z3 C API

Question

I'm trying to use Z3 via the C API and smtlib2 for incremental solving. Unfortunately, I got a segmentation violation when asserting some simple formula, checking it, obtaining its model, asserting something additional and then checking again. This also happens without asserting something new, i.e. when checking, retrieving a model, and checking again. Here is a minimal example to reproduce the error:

#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;
}

I tried with two Z3 versions (4.3.1 on a Mac 64 bit and 4.1 on Ubuntu 64 bit).

I appreciate any help, hints or workarounds - maybe I'm just using the API in a wrong way?

Many thanks,

Elisabeth

One thing to note is that the C API requires that the caller explicitly increment/decrement reference counts to objects, such as the solver. — Nikolaj Bjorner

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2013-04-09T20:03:53

Here is a version of your code using reference counts. It crashes when I delete the reference counting.

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. The C++ API hides all the reference counting details. It is much more convenient to work with.

check; get_model; check causes segfault in Z3 C API

1 Answers