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

fix #5681

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-11-24 13:24:31 +01:00
parent e8f5a29c31
commit 833dd62623
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/c++/z3++.h
View file

@ -1911,7 +1911,7 @@ namespace z3 {
} }
inline expr bvredand(expr const & a) { inline expr bvredand(expr const & a) {
assert(a.is_bv()); assert(a.is_bv());
Z3_ast r = Z3_mk_bvredor(a.ctx(), a); Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
a.check_error(); a.check_error();
return expr(a.ctx(), r); return expr(a.ctx(), r);
} }

18
src/smt/theory_seq.cpp
View file

@ -2206,8 +2206,9 @@ expr_ref theory_seq::elim_skolem(expr* e) {
if (m_sk.is_post(a, x, y) && cache.contains(x) && cache.contains(y)) { if (m_sk.is_post(a, x, y) && cache.contains(x) && cache.contains(y)) {
x = cache[x]; x = cache[x];
y = cache[y]; y = cache[y];
auto mk_max = [&](expr* x, expr* y) { return m.mk_ite(m_autil.mk_ge(x, y), x, y); };
result = m_util.str.mk_length(x); result = m_util.str.mk_length(x);
result = m_util.str.mk_substr(x, y, m_autil.mk_sub(result, y)); result = m_util.str.mk_substr(x, mk_max(y,m_autil.mk_int(0)), m_autil.mk_sub(result, y));
trail.push_back(result); trail.push_back(result);
cache.insert(a, result); cache.insert(a, result);
todo.pop_back(); todo.pop_back();
@ -2277,16 +2278,14 @@ expr_ref theory_seq::elim_skolem(expr* e) {
args.reset(); args.reset();
for (expr* arg : *to_app(a)) { for (expr* arg : *to_app(a)) {
if (cache.find(arg, b)) { if (cache.find(arg, b))
args.push_back(b); args.push_back(b);
} else
else {
todo.push_back(arg); todo.push_back(arg);
}
} }
if (args.size() < to_app(a)->get_num_args()) {
if (args.size() < to_app(a)->get_num_args())
continue; continue;
}
if (m_util.is_skolem(a)) { if (m_util.is_skolem(a)) {
IF_VERBOSE(0, verbose_stream() << "unhandled skolem " << mk_pp(a, m) << "\n"); IF_VERBOSE(0, verbose_stream() << "unhandled skolem " << mk_pp(a, m) << "\n");
@ -2367,11 +2366,12 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
if (r == l_true) { if (r == l_true) {
model_ref mdl; model_ref mdl;
k.get_model(mdl); k.get_model(mdl);
TRACE("seq", tout << "failed to validate\n" << *mdl << "\n");
IF_VERBOSE(0, IF_VERBOSE(0,
verbose_stream() << r << "\n" << fmls << "\n"; verbose_stream() << r << "\n" << fmls << "\n";
verbose_stream() << *mdl.get() << "\n"; verbose_stream() << *mdl.get() << "\n";
k.display(verbose_stream())); k.display(verbose_stream()) << "\n");
UNREACHABLE(); //UNREACHABLE();
} }
} }