fix #7521 (#7531)

Z3Prover · Jan 27, 2025 · f574950 · f574950
1 parent 5634dc5
commit f574950
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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;