fixing #2448 and #2445 and #2443

NikolajBjorner · NikolajBjorner · commit c4480337c4d4 · 2019-08-02T15:06:34.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -2519,7 +2519,6 @@ bool theory_seq::occurs(expr* a, expr* b) {
         b = m_todo.back();
         if (a == b || m.is_ite(b)) {
             m_todo.reset();
-            std::cout << " yes\n";
             return true;
         }
         m_todo.pop_back();

Original file line number	Diff line number	Diff line change
`@@ -2519,7 +2519,6 @@ bool theory_seq::occurs(expr* a, expr* b) {`
`2519`	`2519`	`b = m_todo.back();`
`2520`	`2520`	`if (a == b \|\| m.is_ite(b)) {`
`2521`	`2521`	`m_todo.reset();`
`2522`		`- std::cout << " yes\n";`
`2523`	`2522`	`return true;`
`2524`	`2523`	`}`
`2525`	`2524`	`m_todo.pop_back();`