From a2207bc35cbbdb86d4d8b864eb3213b227f584d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Apr 2013 07:52:55 -0700 Subject: [PATCH] stash --- src/muz_qe/dl_mk_karr_invariants.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 77b52f2b9..458f46628 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -387,6 +387,8 @@ namespace datalog { } lbool is_sat = m_hb.saturate(); TRACE("dl_verbose", m_hb.display(tout);); + // TBD: actually transition function can be unsat. + // in this case the rule can be removed. SASSERT(is_sat == l_true); dst.reset(); unsigned basis_size = m_hb.get_basis_size();