mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix #3849

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-07 19:28:02 -07:00
parent 7fc9eb11db
commit 0e78f092b5
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/muz/transforms/dl_mk_elim_term_ite.cpp
View file

@ -165,7 +165,8 @@ namespace datalog {
head = ground(head);
fml2 = m.mk_implies(body, head);
SASSERT(!has_term_ite(fml2));
if (has_term_ite(fml2))
return false;
app_ref_vector consts(m);
collect_uninterp_consts(fml2, consts);
fml2 = mk_forall(m, consts.size(), consts.c_ptr(), fml2);