Do not purify ground Boolean subterms in quantifier bodies (cvc5#11654)

Fixes cvc5/cvc5-projects#763.

More generally, this issue suggests it is not safe to introduce
purification skolems for any Boolean term, as this can make them
allocated as an "internal-only" SAT literal, where if later the same
purification skolem is introduced as a Boolean term skolem, the theory
solvers will not be notified. This will require more thought.

Author: ajreynol

src/theory/quantifiers/ematching/trigger.cpp

@@ -160,7 +160,7 @@ uint64_t Trigger::addInstantiations()
     eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
     for (const Node& gt : d_groundTerms)
     {
-      if (!ee->hasTerm(gt))
+      if (!ee->hasTerm(gt) && !gt.getType().isBoolean())
       {
         Node k = SkolemManager::mkPurifySkolem(gt);
         Node eq = k.eqNode(gt);

test/regress/cli/CMakeLists.txt

@@ -1572,6 +1572,7 @@ set(regress_0_tests
   regress0/quantifiers/proj-issue152-2-non-std-nterm-ext-rew.smt2
   regress0/quantifiers/proj-issue512-has-skolem.smt2
   regress0/quantifiers/proj-issue608-mbqi-cegqi.smt2
+  regress0/quantifiers/proj-issue763-no-gt-purify-bool.smt2
   regress0/quantifiers/pure_dt_cbqi.smt2
   regress0/quantifiers/qarray-sel-over-store.smt2
   regress0/quantifiers/qbv-inequality2.smt2

test/regress/cli/regress0/quantifiers/proj-issue763-no-gt-purify-bool.smt2

@@ -0,0 +1,7 @@
+; COMMAND-LINE: --mbqi
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x5 (Seq Bool))
+(declare-const x (Array Bool Bool))
+(assert (not (select x (exists ((_x (Seq Bool))) (forall ((x (Array Bool Bool))) (select x (seq.prefixof x5 _x)))))))
+(check-sat)