diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 38b1c7149..0ef8c7992 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -3488,7 +3488,7 @@ lbool context::handle_unknown(pob &n, const datalog::rule *r, model &model) { } // model \models reach_fact && Tr && pob if (model.is_true(n.pt().get_transition(*r)) && model.is_true(n.post()) && - n.pt().mk_mdl_rf_consistent(r, model)) { + r->get_uninterpreted_tail_size() == 0 && n.pt().mk_mdl_rf_consistent(r, model)) { return l_true; } return l_undef;