From 9b01a5153eb8a09377e0d71f66094779f7119ba3 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 18 Sep 2017 14:44:05 -0400 Subject: [PATCH] fix generation of symbolic automata with no moves but accepting initial state --- src/math/automata/symbolic_automata_def.h | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index c89080d3d..3be6a1da0 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -451,7 +451,15 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_produ } } if (mvs1.empty()) { - return alloc(automaton_t, m); + if (a.is_final_state(a.init()) && b.is_final_state(b.init())) { + // 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(); + final.push_back(0); + return alloc(automaton_t, m, 0, final, mvs1); + } else { + return alloc(automaton_t, m); + } } else { return alloc(automaton_t, m, 0, final, mvs1);