mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix copy function

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-17 23:50:48 -08:00
parent df6b1a707e
commit 00f5308a0e
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/goal.cpp
View file

@ -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) {

3
src/tactic/goal.h
View file

@ -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)); }