Mark quantifier instances that lead to conflicts as relevant (#10064)

This patch fixes a corner case where quantifier conflicts can create
fresh terms that aren't marked as relevant.
I couldn't easily produce a minimal query that this patch turns stable,
nor did the patch stabilize the query I have been working on, but I
think the example below still illustrates the problem:

```
(set-option :auto_config false)
(set-option :type_check true)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)

(declare-fun R (Int) Bool)
(declare-fun S (Int) Bool)
(declare-fun dummy (Int) Bool)

(assert (or (R 0) (dummy 0)))

(assert (forall ((x Int)) (! 
    (and (not (R x)) (not (S x)))
    :pattern ((R x))
    :qid not_r_not_s
)))

(assert (forall ((x Int)) (! 
    (S x)
    :pattern ((S x))
    :qid s_true
)))
(check-sat)
```

The query is unstable (due to the same interaction between relevancy and
triggers in https://github.com/Z3Prover/z3/issues/7444): if the solver
assigns `(dummy 0)` first, it returns `unknown`.

If the solver assigns `(R 0)` first, we would expect an `unsat`. The
current implementation returns `unknown` because `not_r_not_s` leads to
a quantifier conflict, which creates `S(x)` without marking it (or any
of its ancestors) as relevant.

---------

Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/smt_context.h

@@ -1733,8 +1733,16 @@ namespace smt {
 
         void internalize_instance(expr * body, proof * pr, unsigned generation) {
             internalize_assertion(body, pr, generation);
-            if (relevancy())
+            if (relevancy()) {
+                // if the instantiation creates a conflict, we backtrack immediately.
+                // to retain the conflict clause being relevant we mark it here.
+                // if the instantiation does not create a conflict, default relevancy propagation applies.
+                if (inconsistent() && is_app(body)) {
+                    for (auto arg : *to_app(body))
+                        mark_as_relevant(arg);
+                }
                 m_case_split_queue->internalize_instance_eh(body, generation);
+            }
         }
 
         unsigned get_unsat_core_size() const {