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

qe_lite: fix crash when formula has var def with concat, e.g.

Browse source 
(assert (forall ((a (_ BitVec 4)) (b (_ BitVec 4)))
  (not (and (= a (bvshl #x1 b))
            (= ((_ extract 3 2) b) #b00)))))
This commit is contained in:
Nuno Lopes 2020-01-30 14:07:47 +00:00
parent 1f0bd04e50
commit bb5edb7c65
1 changed files with 9 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/qe/qe_lite.cpp
View file

@ -143,11 +143,6 @@ namespace {
for (unsigned i = 0; i < definitions.size(); i++) { for (unsigned i = 0; i < definitions.size(); i++) {
if (definitions[i] == nullptr) if (definitions[i] == nullptr)
continue; continue;
if (is_sub_extract(vars[i]->get_idx(), definitions[i])) {
order.push_back(i);
done.mark(definitions[i]);
continue;
}
var * v = vars[i]; var * v = vars[i];
SASSERT(v->get_idx() == i); SASSERT(v->get_idx() == i);
SASSERT(todo.empty()); SASSERT(todo.empty());
@ -172,6 +167,10 @@ namespace {
visiting.reset_mark(t); visiting.reset_mark(t);
definitions[vidx] = nullptr; definitions[vidx] = nullptr;
} }
else if (is_sub_extract(vidx, definitions[vidx])) {
order.push_back(vidx);
done.mark(definitions[vidx]);
}
else { else {
visiting.mark(t); visiting.mark(t);
fr.second = 1; fr.second = 1;
@ -183,10 +182,8 @@ namespace {
else { else {
SASSERT(fr.second == 1); SASSERT(fr.second == 1);
visiting.reset_mark(t); visiting.reset_mark(t);
if (!done.is_marked(t)) { if (!done.is_marked(t) && definitions.get(vidx, nullptr) != nullptr) {
if (definitions.get(vidx, nullptr) != nullptr) order.push_back(vidx);
order.push_back(vidx);
done.mark(t);
} }
} }
done.mark(t); done.mark(t);
@ -194,7 +191,6 @@ namespace {
break; break;
case AST_QUANTIFIER: case AST_QUANTIFIER:
UNREACHABLE(); UNREACHABLE();
todo.pop_back();
break; break;
case AST_APP: case AST_APP:
num = to_app(t)->get_num_args(); num = to_app(t)->get_num_args();
@ -210,7 +206,6 @@ namespace {
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();
todo.pop_back();
break; break;
} }
} }
@ -325,8 +320,6 @@ namespace {
} }
void get_elimination_order() { void get_elimination_order() {
m_order.reset();
TRACE("top_sort", TRACE("top_sort",
tout << "DEFINITIONS: " << std::endl; tout << "DEFINITIONS: " << std::endl;
for(unsigned i = 0; i < m_map.size(); i++) for(unsigned i = 0; i < m_map.size(); i++)
@ -901,6 +894,7 @@ namespace {
// ------------------------------------------------------------ // ------------------------------------------------------------
// fm_tactic adapted to eliminate designated de-Bruijn indices. // fm_tactic adapted to eliminate designated de-Bruijn indices.
namespace fm {
typedef ptr_vector<app> clauses; typedef ptr_vector<app> clauses;
typedef unsigned var; typedef unsigned var;
typedef int bvar; typedef int bvar;
@ -2215,6 +2209,7 @@ namespace {
} }
}; };
} // namespace fm
} // anonymous namespace } // anonymous namespace
class qe_lite::impl { class qe_lite::impl {
@ -2266,7 +2261,7 @@ public:
private: private:
ast_manager& m; ast_manager& m;
eq_der m_der; eq_der m_der;
fm m_fm; fm::fm m_fm;
ar_der m_array_der; ar_der m_array_der;
elim_star m_elim_star; elim_star m_elim_star;
th_rewriter m_rewriter; th_rewriter m_rewriter;