Segmentation fault using the Z3 API with C++

I have a project that generated big smtlib2 problems as strings and it solved them by writing the problems to a file and then calling a solver via exec(). I'm trying to integrate Z3 to solve it via API, because the problem is inherently incremental, and thus the learning by the solver will be used between calls.

The problems I face are:

1. I get a segfault when I assert something using the function 'z3_assert_str' shown below.
2. The trace file is always empty, it seems the config parameters are not working or not corretly set.

I have tried with Z3 4.4.0 and trunk, directly from github.

What am I doing wrong?

---

Here are the important bits from the class:

foo.h

In this class I maintain two vectors (v_symbols and v_func_decl) to keep track of what I have inserted in the problem, so then I can call "Z3_parse_smtlib2_string"

// attributes of foo.h
z3::config * cfg;
z3::context * c;
z3::solver * s;

std::vector<Z3_symbol> v_symbols;
std::vector<Z3_func_decl> v_func_decl;

// main z3 interaction function
void z3_assert_str(std::string s);

foo.cpp

// in the class constructor, I initialize the 
// z3 structures as follows
cfg = new z3::config(); 
cfg->set("trace", true);
cfg->set("trace_file_name", "z3.log");
c = new z3::context(*cfg);
s = new z3::solver(*c);

// then I keep adding integer vars
expr foobar = c->int_const(obj.c_str());
v_symbols.push_back(foobar.decl().name());
v_func_decl.push_back(foobar.decl());  

// and Uninterpreted Functions (UF)
func_decl f = c->function(f_name.c_str(), sort_vec, z3_int_sort);
v_symbols.push_back(f.name());
v_func_decl.push_back(f);

// and finally the funcion that asserts a smtlib2 string
void encodingUFVisitorZ3::z3_assert_str(std::string constraint) {
    try {
        Z3_ast ast = Z3_parse_smtlib2_string(*c,constraint.c_str(),
                0, 0, 0,
                v_symbols.size(),
                &v_symbols[0],
                &v_func_decl[0]);

        z3::expr constr = to_expr(*c, ast);
        s->add(constr);
    } catch (z3::exception ex) {
        std::cout << "failed: " << ex << "\n";
    }
}

segfault

Program received signal SIGSEGV, Segmentation fault.
0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
372     bool is_right_associative() const { return m_right_assoc; }
(gdb) bt
#0  0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
#1  0x00007ffff730d7b5 in func_decl::is_right_associative (this=0xa623d8) at ../src/ast/ast.h:591
#2  0x00007ffff730375b in ast_manager::mk_app (this=0x8a4058, decl=0xa623d8, num_args=2, args=0xa6d9a0) at ../src/ast/ast.cpp:2046
#3  0x00007ffff703da03 in cmd_context::mk_app (this=0x7fffffffd2e0, s=..., num_args=2, args=0xa6d9a0, num_indices=0, indices=0x0, range=0x0, result=...) at ../src/cmd_context/cmd_context.cpp:998
#4  0x00007ffff701cfb3 in smt2::parser::pop_app_frame (this=0x7fffffffca80, fr=0x8c1bc0) at ../src/parsers/smt2/smt2parser.cpp:1526
#5  0x00007ffff701eafc in smt2::parser::pop_expr_frame (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1663
#6  0x00007ffff701edd3 in smt2::parser::parse_expr (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1696
#7  0x00007ffff7020910 in smt2::parser::parse_assert (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1957
#8  0x00007ffff7022ca5 in smt2::parser::parse_cmd (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2319
#9  0x00007ffff7023cb6 in smt2::parser::operator() (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2470
#10 0x00007ffff7012df1 in parse_smt2_commands (ctx=..., is=..., interactive=false, ps=...) at ../src/parsers/smt2/smt2parser.cpp:2519
#11 0x00007ffff68de38b in parse_smtlib2_stream (exec=false, c=0x8a3148, is=..., num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:272
#12 0x00007ffff68de664 in Z3_parse_smtlib2_string (c=0x8a3148, str=0xa63758 "(assert (= (at plane1 0) city1))", num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:294
#13 0x0000000000529e38 in encodingUFVisitorZ3::z3_assert_str (this=0x8a2220, constraint=...) at encodingUFVisitorZ3.cpp:308
#14 0x0000000000527f4b in encodingUFVisitorZ3::assertInitialState (this=0x8a2220) at encodingUFVisitorZ3.cpp:118
#15 0x000000000052977d in encodingUFVisitorZ3::solve (this=0x8a2220) at encodingUFVisitorZ3.cpp:238
#16 0x0000000000479854 in PDDLProblem::solve (this=0x84c590) at PDDLProblem.cpp:687
#17 0x000000000053afd1 in main (argc=9, argv=0x7fffffffe018) at main.cpp:203