CODEWITHSUNDEEP
z3
Dan
Dan

Reputation: 1547

Z3 API: Crash when parsing fixed point SMTLib string

I am trying to use the C/C++ API of Z3 to parse fixed point constraints in the SMTLib2 format (specifically files produced by SeaHorn). However, my application crashes when parsing the string (I am using the Z3_fixedpoint_from_string method). The Z3 version I'm working with is version 4.5.1 64 bit.

The SMTLib file I try to parse works find with the Z3 binary, which I have compiled from the sources, but it runs into a segmentation fault when calling Z3_fixedpoint_from_string. I narrowed the problem down to the point that I think the issue is related to adding relations to the fixed point context. A simple example that produces a seg fault on my machine is the following:

#include "z3.h"

int main()
{
    Z3_context c = Z3_mk_context(Z3_mk_config());
    Z3_fixedpoint f = Z3_mk_fixedpoint(c);

    Z3_fixedpoint_from_string (c, f, "(declare-rel R ())");

    Z3_del_context(c);
}

Running this code with valgrind reports a lot of invalid reads and writes. So, either this is not how the API is supposed to be used, or there is a problem somewhere. Unfortunately, I could not find any examples on how to use the fixed point engine programmatically. However, calling Z3_fixedpoint_from_string (c, f, "(declare-var x Int)"); for instance works just fine.

BTW, where is Z3_del_fixedpoint()?

Upvotes: 1

Views: 147

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The fixedpoint object "f" is reference counted. the caller is responsible for taking a reference count immediately after it is created. It is easier to use C++ smart pointers to control this, similar to how we control it for other objects. The C++ API does not have a wrapper for fixedpoint objects so you would have to create your own in the style of other wrappers.

Instead of del_fixedpoint one uses reference counters.

class fixedpoint : public object {
     Z3_fixedpoint m_fp;
public:
    fixedpoint(context& c):object(c) { mfp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
    ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
    operator Z3_fixedpoint() const { return m_fp; }

    void from_string(char const* s) {
         Z3_fixedpoint_from_string (ctx(), m_fp, s);
    }

};

int main()
{
   context c;
   fixedpoint f(c);
   f.from_string("....");       
}

Upvotes: 1

Related Questions