From 00f5308a0e515fa375f0ac41beab41dea292c1e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Nov 2017 23:50:48 -0800 Subject: [PATCH] fix copy function Signed-off-by: Nikolaj Bjorner --- src/tactic/goal.cpp | 2 ++ src/tactic/goal.h | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 7a98be3f1..778c3804b 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -105,6 +105,8 @@ void goal::copy_to(goal & target) const { SASSERT(target.m_core_enabled == m_core_enabled); target.m_inconsistent = m_inconsistent; target.m_precision = mk_union(prec(), target.prec()); + target.m_mc = m_mc.get(); + target.m_pc = m_pc.get(); } void goal::push_back(expr * f, proof * pr, expr_dependency * d) { diff --git a/src/tactic/goal.h b/src/tactic/goal.h index 275c80060..73fbb6f17 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -75,6 +75,7 @@ protected: unsigned get_not_idx(expr * f) const; void shrink(unsigned j); void reset_core(); + public: goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false); @@ -107,7 +108,7 @@ public: void copy_to(goal & target) const; void copy_from(goal const & src) { src.copy_to(*this); } - + void assert_expr(expr * f, proof * pr, expr_dependency * d); void assert_expr(expr * f, expr_dependency * d); void assert_expr(expr * f, expr * d) { assert_expr(f, m().mk_leaf(d)); }