From 9b01a5153eb8a09377e0d71f66094779f7119ba3 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 18 Sep 2017 14:44:05 -0400 Subject: [PATCH 1/2] 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); From 6ddc5495570a15547f5f098dafd7e9de11c68ac1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Sep 2017 12:21:01 -0700 Subject: [PATCH 2/2] fix #1258 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index bd8572d73..0bb76cd90 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2335,7 +2335,12 @@ namespace smt { lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX); vector > coeffs; rational coeff; - if (m_solver->is_term(vi)) { + if (vi == UINT_MAX) { + has_shared = false; + blocker = m.mk_false(); + return inf_eps(rational::one(), inf_rational()); + } + else if (m_solver->is_term(vi)) { const lp::lar_term& term = m_solver->get_term(vi); for (auto & ti : term.m_coeffs) { coeffs.push_back(std::make_pair(ti.second, ti.first));