mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Fix issue https://z3.codeplex.com/workitem/37

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-06-06 18:29:29 -07:00
parent f4f1c63abb
commit 2b59f2ecc2
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -21,7 +21,7 @@ Notes:
#include"goal_num_occurs.h" #include"goal_num_occurs.h"
#include"cooperate.h" #include"cooperate.h"
#include"ast_ll_pp.h" #include"ast_ll_pp.h"
#include"ast_smt2_pp.h" #include"ast_pp.h"
struct ctx_simplify_tactic::imp { struct ctx_simplify_tactic::imp {
struct cached_result { struct cached_result {
@ -105,6 +105,7 @@ struct ctx_simplify_tactic::imp {
} }
bool shared(expr * t) const { bool shared(expr * t) const {
TRACE("ctx_simplify_tactic_bug", tout << mk_pp(t, m) << "\n";);
return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1; return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1;
} }
@ -242,12 +243,13 @@ struct ctx_simplify_tactic::imp {
} }
void assert_expr(expr * t, bool sign) { void assert_expr(expr * t, bool sign) {
expr * p = t;
if (m.is_not(t)) { if (m.is_not(t)) {
t = to_app(t)->get_arg(0); t = to_app(t)->get_arg(0);
sign = !sign; sign = !sign;
} }
bool mk_scope = true; bool mk_scope = true;
if (shared(t)) { if (shared(t) || shared(p)) {
push(); push();
mk_scope = false; mk_scope = false;
assert_eq_core(t, sign ? m.mk_false() : m.mk_true()); assert_eq_core(t, sign ? m.mk_false() : m.mk_true());