Z3 in multithreaded environment #698
Description
Hi,
I am currently writing my Bachelor Thesis and we try to parallelize hybrid systems verification. At some point we use z3. Each time we create a new z3::context object and a new solver, so we expected that we would not run into errors when using multiple threads.
This is roughly what is happening:
z3::context c;
z3::solver z3Solver(c);
// create formula and objective
z3::expr formula = createFormula<Number>(_point, mConstraintMatrix, mConstraintVector, c);
// inform and add constraints
z3Solver.add(formula);
// verify and set result
return (z3::sat == z3Solver.check())
Single threaded, this is working like a charm. When we use more than one thread we get a segfault with the following backtrace.
#0 0x00007ffff787ec43 in void mpz_manager<true>::set<0>(mpz&, int, unsigned int) () from /lib/libz3.so
#1 0x00007ffff787effe in mpz_manager<true>::big_div(mpz const&, mpz const&, mpz&) () from /lib/libz3.so
#2 0x00007ffff6cc480f in mpq_manager<true>::rat_sub(mpq const&, mpq const&, mpq&) () from /lib/libz3.so
#3 0x00007ffff6cc45ea in rational::operator-=(rational const&) () from /lib/libz3.so
#4 0x00007ffff70a8b94 in smt::theory_arith<smt::mi_ext>::select_lg_error_var(bool) () from /lib/libz3.so
#5 0x00007ffff70a3183 in smt::theory_arith<smt::mi_ext>::make_feasible() () from /lib/libz3.so
#6 0x00007ffff70a41f0 in smt::theory_arith<smt::mi_ext>::propagate_core() () from /lib/libz3.so
#7 0x00007ffff718978d in smt::context::propagate() () from /lib/libz3.so
#8 0x00007ffff718e4f0 in smt::context::bounded_search() () from /lib/libz3.so
#9 0x00007ffff718d938 in smt::context::search() () from /lib/libz3.so
#10 0x00007ffff718d7e3 in smt::context::setup_and_check(bool) () from /lib/libz3.so
#11 0x00007ffff7048be9 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#12 0x00007ffff75bc90a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#13 0x00007ffff75d25d3 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#14 0x00007ffff75d28c0 in check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) () from /lib/libz3.so
#15 0x00007ffff74b2781 in tactic2solver::check_sat_core(unsigned int, expr* const*) () from /lib/libz3.so
#16 0x00007ffff74b366b in solver_na2as::check_sat(unsigned int, expr* const*) () from /lib/libz3.so
#17 0x00007ffff74b07d2 in combined_solver::check_sat(unsigned int, expr* const*) () from /lib/libz3.so
#18 0x00007ffff6d2019e in _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) () from /lib/libz3.so
#19 0x00007ffff6d20050 in Z3_solver_check () from /lib/libz3.so
#20 0x0000000001338c7e in z3::solver::check (this=0x7fffedd14870) at /usr/include/z3++.h:1703
Any hints what we are doing wrong or is z3 not supposed to be used in a multithreaded environment?
Kind regards,
Johannes