From d89c39cbe2bb862daff2c183a79361360f7e2dc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Feb 2016 08:36:25 -0800 Subject: [PATCH] apply t() Signed-off-by: Nikolaj Bjorner --- src/math/automata/symbolic_automata_def.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index 6cb3d6339..db6172d49 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -39,7 +39,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_total refs_t vs(m); for (unsigned j = 0; j < mvs.size(); ++j) { - vs.push_back(mvs[j]()); + vs.push_back(mvs[j].t()); } ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m); lbool is_sat = m_ba.is_sat(cond); @@ -64,6 +64,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim if (a.is_empty()) { return a.clone(); } + if (a.is_epsilon()) { return a.clone(); }