From cd434d8bd5c63c35b6faa79804557969326f7b60 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Mar 2020 17:49:48 -0700
Subject: [PATCH] fix #3420

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qsat.cpp         | 1 +
 src/sat/sat_probing.cpp | 5 +++--
 src/smt/theory_seq.cpp  | 1 +
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 4dcc41582..33337057a 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -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);        
diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index 154d460a4..bfb33551f 100644
--- a/src/sat/sat_probing.cpp
+++ b/src/sat/sat_probing.cpp
@@ -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;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3e8ef96eb..a62351edf 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -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;
     }