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

fix location of level retrieval

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-15 17:29:46 -08:00
parent 8fc58e1ace
commit d3805bbdf6
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -110,6 +110,9 @@ public:
bool lo, s; bool lo, s;
expr* t1; expr* t1;
rational n; rational n;
if (!shared(t)) {
return;
}
if (is_bound(t, t1, lo, s, n)) { if (is_bound(t, t1, lo, s, n)) {
if (sign) { if (sign) {
// !(n <= t1) <=> t1 <= n - 1 // !(n <= t1) <=> t1 <= n - 1

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

@ -202,8 +202,8 @@ struct ctx_simplify_tactic::imp {
} }
void cache_core(expr * from, expr * to) { void cache_core(expr * from, expr * to) {
TRACE("ctx_simplify_tactic_cache", tout << "caching\n" << mk_ismt2_pp(from, m) << "\n--->\n" << mk_ismt2_pp(to, m) << "\n";);
unsigned id = from->get_id(); unsigned id = from->get_id();
TRACE("ctx_simplify_tactic_cache", tout << "caching " << id << " @ " << scope_level() << "\n" << mk_ismt2_pp(from, m) << "\n--->\n" << mk_ismt2_pp(to, m) << "\n";);
m_cache.reserve(id+1); m_cache.reserve(id+1);
cache_cell & cell = m_cache[id]; cache_cell & cell = m_cache[id];
void * mem = m_allocator.allocate(sizeof(cached_result)); void * mem = m_allocator.allocate(sizeof(cached_result));
@ -270,11 +270,11 @@ struct ctx_simplify_tactic::imp {
if (num_scopes == 0) if (num_scopes == 0)
return; return;
SASSERT(num_scopes <= scope_level()); SASSERT(num_scopes <= scope_level());
unsigned lvl = scope_level();
m_simp->pop(num_scopes); m_simp->pop(num_scopes);
// restore cache // restore cache
unsigned lvl = scope_level();
for (unsigned i = 0; i < num_scopes; i++) { for (unsigned i = 0; i < num_scopes; i++) {
restore_cache(lvl); restore_cache(lvl);
lvl--; lvl--;