mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

fix regression introduced by using ref-vectors on non-ref'ed output parameters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-18 17:22:47 -07:00
parent 5d0db6d256
commit 4cb57cd4da
2 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/tactic/goal.cpp
View file

@ -136,7 +136,7 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
} }
} }
void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) { void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) {
if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
if (!save_first) { if (!save_first) {
push_back(f, 0, d); push_back(f, 0, d);
@ -175,7 +175,7 @@ void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
} }
else { else {
if (!pol) { if (!pol) {
curr = m().mk_not(curr); curr = m().mk_not(curr);
tmp_exprs.push_back(curr); tmp_exprs.push_back(curr);
} }
if (save_first) { if (save_first) {
@ -242,8 +242,10 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
return; return;
if (proofs_enabled()) if (proofs_enabled())
slow_process(f, pr, d); slow_process(f, pr, d);
else else {
quick_process(false, f, d); expr_ref fr(f, m());
quick_process(false, fr, d);
}
} }
void goal::assert_expr(expr * f, expr_dependency * d) { void goal::assert_expr(expr * f, expr_dependency * d) {
@ -279,13 +281,14 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
} }
} }
else { else {
quick_process(true, f, d); expr_ref fr(f, m());
quick_process(true, fr, d);
if (!m_inconsistent) { if (!m_inconsistent) {
if (m().is_false(f)) { if (m().is_false(fr)) {
push_back(f, 0, d); push_back(f, 0, d);
} }
else { else {
m().set(m_forms, i, f); m().set(m_forms, i, fr);
if (unsat_core_enabled()) if (unsat_core_enabled())
m().set(m_dependencies, i, d); m().set(m_dependencies, i, d);
} }

2
src/tactic/goal.h
View file

@ -62,7 +62,7 @@ protected:
unsigned m_precision:2; // PRECISE, UNDER, OVER. unsigned m_precision:2; // PRECISE, UNDER, OVER.
void push_back(expr * f, proof * pr, expr_dependency * d); void push_back(expr * f, proof * pr, expr_dependency * d);
void quick_process(bool save_first, expr * & f, expr_dependency * d); void quick_process(bool save_first, expr_ref & f, expr_dependency * d);
void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);