mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
avoid infinite loop between is-nullable and mk-bool-app
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4dc7089cc4
commit
9a642215eb
|
@ -437,28 +437,26 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const*
|
|||
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
expr* args_i = args[i];
|
||||
expr* x = nullptr;
|
||||
expr* y = nullptr;
|
||||
expr* z = nullptr;
|
||||
if (str().is_in_re(args_i, x, y)) {
|
||||
expr* x = nullptr, *y = nullptr, *z = nullptr;
|
||||
if (str().is_in_re(args_i, x, y) && !str().is_empty(x)) {
|
||||
if (in_re.find(x, z)) {
|
||||
in_re[x] = is_and ? re().mk_inter(z, y) : re().mk_union(z, y);
|
||||
found_pair = true;
|
||||
}
|
||||
else {
|
||||
in_re.insert(x, y);
|
||||
found_pair |= not_in_re.contains(x);
|
||||
}
|
||||
found_pair |= not_in_re.contains(x);
|
||||
}
|
||||
else if (m().is_not(args_i, arg) && str().is_in_re(arg, x, y)) {
|
||||
else if (m().is_not(args_i, arg) && str().is_in_re(arg, x, y) && !str().is_empty(x)) {
|
||||
if (not_in_re.find(x, z)) {
|
||||
not_in_re[x] = is_and ? re().mk_union(z, y) : re().mk_inter(z, y);
|
||||
found_pair = true;
|
||||
}
|
||||
else {
|
||||
not_in_re.insert(x, y);
|
||||
found_pair |= in_re.contains(x);
|
||||
}
|
||||
found_pair |= in_re.contains(x);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -1497,7 +1497,7 @@ lbool core::check(vector<lemma>& l_vec) {
|
|||
m_tangents.tangent_lemma();
|
||||
}
|
||||
|
||||
if (l_vec.empty() && !done() && m_nla_settings.run_nra()) {
|
||||
if (!done() && m_nla_settings.run_nra()) {
|
||||
ret = m_nra.check();
|
||||
m_stats.m_nra_calls ++;
|
||||
}
|
||||
|
|
|
@ -73,6 +73,8 @@ struct solver::imp {
|
|||
}
|
||||
// TBD: add variable bounds?
|
||||
|
||||
m_nlsat->display(std::cout);
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
r = m_nlsat->check();
|
||||
|
|
Loading…
Reference in a new issue