mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
add back assertion for #3849
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4651bffafc
commit
c4b52edb29
|
@ -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);
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue