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

qe_lite> fix crash in is_var_eq()

Browse source 
(by me & Nikolaj)

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-03-25 09:53:11 -07:00
parent b1fc6a5cac
commit b427958b9e
1 changed files with 14 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/muz_qe/qe_lite.cpp
View file

@ -201,9 +201,15 @@ namespace eq {
return (*m_is_variable)(e); return (*m_is_variable)(e);
} }
bool is_neg_var(ast_manager & m, expr * e) { bool is_neg_var(ast_manager & m, expr * e, var*& v) {
expr* e1; expr* e1;
return m.is_not(e, e1) && is_variable(e1); if (m.is_not(e, e1) && is_variable(e1)) {
v = to_var(e1);
return true;
}
else {
return false;
}
} }
@ -328,18 +334,19 @@ namespace eq {
bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) { bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) {
expr* lhs, *rhs; expr* lhs, *rhs;
var* v;
// (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases
if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) { if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) {
// (iff (not VAR) t) (iff t (not VAR)) cases // (iff (not VAR) t) (iff t (not VAR)) cases
if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) { if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) {
if (!is_neg_var(m, lhs)) { if (!is_neg_var(m, lhs, v)) {
std::swap(lhs, rhs); std::swap(lhs, rhs);
} }
if (!is_neg_var(m, lhs)) { if (!is_neg_var(m, lhs, v)) {
return false; return false;
} }
vs.push_back(to_var(lhs)); vs.push_back(v);
ts.push_back(m.mk_not(rhs)); ts.push_back(m.mk_not(rhs));
TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
return true; return true;
@ -378,9 +385,9 @@ namespace eq {
} }
// VAR = false case // VAR = false case
if (is_neg_var(m, e)) { if (is_neg_var(m, e, v)) {
ts.push_back(m.mk_false()); ts.push_back(m.mk_false());
vs.push_back(to_var(to_app(e)->get_arg(0))); vs.push_back(v);
TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
return true; return true;
} }