mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
fix Boolean argument
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8566d88b99
commit
6bd87f837a
|
@ -213,7 +213,7 @@ class parallel_tactic : public tactic {
|
||||||
solver_state* clone() {
|
solver_state* clone() {
|
||||||
SASSERT(!m_cubes.empty());
|
SASSERT(!m_cubes.empty());
|
||||||
ast_manager& m = m_solver->get_manager();
|
ast_manager& m = m_solver->get_manager();
|
||||||
ast_manager* new_m = alloc(ast_manager, m, m.proof_mode());
|
ast_manager* new_m = alloc(ast_manager, m, true);
|
||||||
ast_translation tr(m, *new_m);
|
ast_translation tr(m, *new_m);
|
||||||
solver* s = m_solver.get()->translate(*new_m, m_params);
|
solver* s = m_solver.get()->translate(*new_m, m_params);
|
||||||
solver_state* st = alloc(solver_state, new_m, s, m_params);
|
solver_state* st = alloc(solver_state, new_m, s, m_params);
|
||||||
|
|
Loading…
Reference in a new issue