From a921b4ff4ad331a3b0800cdcb88d2125d9b95ab2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Oct 2019 18:19:13 -0700
Subject: [PATCH] fix #2643 - fuzzers are here to get you @lorisdanton

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp         | 6 ++++--
 src/math/automata/symbolic_automata_def.h | 9 ++++++---
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 3a75c6522..8907a8376 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -251,7 +251,7 @@ eautomaton* re2automaton::operator()(expr* e) {
     if (r) {        
         r->compress(); 
         bool_rewriter br(m);
-        TRACE("seq", display_expr1 disp(m); r->display(tout, disp););
+        TRACE("seq", display_expr1 disp(m); r->display(tout << mk_pp(e, m) << " -->\n", disp););
     }
     return r;
 } 
@@ -348,7 +348,9 @@ eautomaton* re2automaton::re2aut(expr* e) {
         return a.detach();
     }
     else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
-        return m_sa->mk_product(*a, *b);
+        eautomaton* r = m_sa->mk_product(*a, *b);
+        TRACE("seq", display_expr1 disp(m); a->display(tout << "a:", disp); b->display(tout << "b:", disp); r->display(tout << "intersection:", disp););
+        return r;
     }
     else {
         TRACE("seq", tout << "not handled " << mk_pp(e, m) << "\n";);
diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index 62f87b135..6b995c8cf 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -381,11 +381,14 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
     unsigned_vector final;
     unsigned_vector a_init, b_init;
     a.get_epsilon_closure(a.init(), a_init);
+    bool a_init_is_final = false, b_init_is_final = false;
     for (unsigned ia : a_init) {
         if (a.is_final_state(ia)) {
+            a_init_is_final = true;
             b.get_epsilon_closure(b.init(), b_init);
             for (unsigned ib : b_init) {
                 if (b.is_final_state(ib)) {
+                    b_init_is_final = true;
                     final.push_back(0);
                     break;
                 }
@@ -438,8 +441,8 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
     }
     
     svector<bool> back_reachable(n, false);
-    for (unsigned i = 0; i < final.size(); ++i) {
-        back_reachable[final[i]] = true;
+    for (unsigned f : final) {
+        back_reachable[f] = true;
     }
     
     unsigned_vector stack(final);
@@ -464,7 +467,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
         }
     }
     if (mvs1.empty()) {
-        if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
+        if (a_init_is_final && b_init_is_final) {
             // special case: automaton has no moves, but the initial state is final on both sides
             // this results in the automaton which accepts the empty sequence and nothing else
             final.clear();