3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

finished fix for #3849 by converting assert into trace

This commit is contained in:
Arie Gurfinkel 2020-04-10 21:09:36 -04:00
parent fdabaa6cd2
commit d53e30ecbe

View file

@ -172,7 +172,7 @@ namespace datalog {
rw(body);
fml2 = m.mk_implies(body, ground(r.get_head()));
SASSERT(!has_term_ite(fml2));
CTRACE("dl", has_term_ite(fml2), tout << "Rule has term-ite after elimination. Giving up\n";);
if (has_term_ite(fml2))
return false;
app_ref_vector consts(m);