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

fix #3915

Browse source
This commit is contained in:
Arie Gurfinkel 2020-04-11 14:16:29 -04:00
parent 2b27aa1ce6
commit 1e96570365
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/muz/spacer/spacer_context.cpp
View file

@ -1623,12 +1623,12 @@ void pred_transformer::init_rules(decl2rel const& pts) {
if (not_inits.empty ()) {m_all_init = true;} if (not_inits.empty ()) {m_all_init = true;}
} }
#ifdef Z3DEBUG // #ifdef Z3DEBUG
static bool is_all_non_null(app_ref_vector const& apps) { // static bool is_all_non_null(app_ref_vector const& apps) {
for (auto *a : apps) if (!a) return false; // for (auto *a : apps) if (!a) return false;
return true; // return true;
} // }
#endif // #endif
void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule) { void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule) {
scoped_watch _t_(m_initialize_watch); scoped_watch _t_(m_initialize_watch);
@ -1659,7 +1659,7 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule)
trans= mk_and (tail); trans= mk_and (tail);
ground_free_vars(trans, var_reprs, aux_vars, ut_size == 0); ground_free_vars(trans, var_reprs, aux_vars, ut_size == 0);
SASSERT(is_all_non_null(var_reprs)); // SASSERT(is_all_non_null(var_reprs));
expr_ref tmp = var_subst(m, false)(trans, var_reprs.size (), (expr*const*)var_reprs.c_ptr()); expr_ref tmp = var_subst(m, false)(trans, var_reprs.size (), (expr*const*)var_reprs.c_ptr());
flatten_and (tmp, side); flatten_and (tmp, side);