mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #3420

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-19 17:49:48 -07:00
parent 5cbcd9a88a
commit cd434d8bd5
3 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/qe/qsat.cpp
View file

@ -1329,6 +1329,7 @@ namespace qe {
}
void collect_statistics(statistics & st) const override {
std::cout << "collect stats\n";
st.copy(m_st);
m_fa.s().collect_statistics(st);
m_ex.s().collect_statistics(st);

5
src/sat/sat_probing.cpp
View file

@ -161,7 +161,9 @@ namespace sat {
if (m_probing_binary) {
watch_list & wlist = s.get_wlist(~l);
for (watched & w : wlist) {
unsigned sz0 = wlist.size();
for (unsigned i = 0; i < wlist.size(); ++i) {
watched & w = wlist[i];
if (!w.is_binary_clause())
continue;
literal l2 = w.get_literal();
@ -169,7 +171,6 @@ namespace sat {
continue;
if (s.value(l2) != l_undef)
continue;
// verbose_stream() << "probing " << l << " " << l2 << " " << m_counter << "\n";
// Note: that try_lit calls propagate, which may update the watch lists.
if (!try_lit(l2, false))
return;

1
src/smt/theory_seq.cpp
View file

@ -2602,6 +2602,7 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
if (!idx_is_zero) rs1.push_back(mk_skolem(m_pre, s, idx));
rs1.push_back(m_util.str.mk_unit(rhs));
rs1.push_back(mk_post(s, idx1));
TRACE("seq", tout << ls1 << "\n"; tout << rs1 << "\n";);
m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps));
return true;
}