From c4b52edb295d06a8fccd56e8d54c642141378d42 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Apr 2020 18:08:40 -0700 Subject: [PATCH] add back assertion for #3849 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_elim_term_ite.cpp | 1 + src/smt/smt_context_pp.cpp | 2 ++ 2 files changed, 3 insertions(+) diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp index a13491eba..218d64d0f 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.cpp +++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp @@ -172,6 +172,7 @@ namespace datalog { rw(body); fml2 = m.mk_implies(body, ground(r.get_head())); + SASSERT(!has_term_ite(fml2)); if (has_term_ite(fml2)) return false; app_ref_vector consts(m); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index a5ec36466..00c23a9f5 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -454,6 +454,7 @@ namespace smt { display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic); TRACE("non_linear", display_lemma_as_smt_problem(tout, num_antecedents, antecedents, consequent, logic);); out.close(); + SASSERT(m_lemma_id != 2); return m_lemma_id; } @@ -497,6 +498,7 @@ namespace smt { ); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); out.close(); + SASSERT(m_lemma_id != 2); return m_lemma_id; }