fix #2262

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/math/automata/automaton.h

@@ -348,6 +348,7 @@ class automaton {
     //
     void compress() {
         SASSERT(!m_delta.empty());
+        TRACE("seq", display(tout););
         for (unsigned i = 0; i < m_delta.size(); ++i) {
             for (unsigned j = 0; j < m_delta[i].size(); ++j) {
                 move const& mv = m_delta[i][j];
@@ -460,6 +461,7 @@ class automaton {
             }
         }
         sinkify_dead_states();
+        TRACE("seq", display(tout););
     }
 
     bool is_sequence(unsigned& length) const {
@@ -559,9 +561,8 @@ class automaton {
     template<class D>
     std::ostream& display(std::ostream& out, D& displayer = D()) const {
         out << "init: " << init() << "\n";
-        out << "final: ";
-        for (unsigned i = 0; i < m_final_states.size(); ++i) out << m_final_states[i] << " ";
-        out << "\n";
+        out << "final: " << m_final_states << "\n";
+
         for (unsigned i = 0; i < m_delta.size(); ++i) {
             moves const& mvs = m_delta[i];
             for (move const& mv : mvs) {
@@ -577,6 +578,22 @@ class automaton {
     }
 private:
 
+    std::ostream& display(std::ostream& out) const {
+        out << "init: " << init() << "\n";
+        out << "final: " << m_final_states << "\n";
+
+        for (unsigned i = 0; i < m_delta.size(); ++i) {
+            moves const& mvs = m_delta[i];
+            for (move const& mv : mvs) {
+                out << i << " -> " << mv.dst() << " ";
+                if (mv.t()) {
+                    out << "if *** "; 
+                }
+                out << "\n";
+            }
+        }
+        return out;
+    }
     void sinkify_dead_states() {
         uint_set dead_states;
         for (unsigned i = 0; i < m_delta.size(); ++i) {
@@ -604,7 +621,9 @@ class automaton {
             }
             to_remove.reset();
         }
-        TRACE("seq", tout << "remove: " << dead_states << "\n";);
+        TRACE("seq", tout << "remove: " << dead_states << "\n"; 
+              tout << "final: " << m_final_states << "\n";
+              );
         for (unsigned s : dead_states) {
             CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";); 
             m_delta[s].reset();

src/math/automata/symbolic_automata_def.h

@@ -379,9 +379,21 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
     pair2id.insert(init_pair, 0);
     moves_t mvs;
     unsigned_vector final;
-    if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
-        final.push_back(0);
+    unsigned_vector a_init, b_init;
+    a.get_epsilon_closure(a.init(), a_init);
+    for (unsigned ia : a_init) {
+        if (a.is_final_state(ia)) {
+            b.get_epsilon_closure(b.init(), b_init);
+            for (unsigned ib : b_init) {
+                if (b.is_final_state(ib)) {
+                    final.push_back(0);
+                    break;
+                }
+            }
+            break;
+        }
     }
+    
     unsigned n = 1;
     moves_t mvsA, mvsB;
     while (!todo.empty()) {