Fix MBQI ho_var term-enumeration timeout regression (iss-6174/small.smt2)

Commit 6fd303c4b ("set the auf flag to false in all cases") additionally
added two Boolean productions to the ho_var instantiation-set enumeration
in smt_model_finder.cpp:

    tn.add_production(m.mk_true());
    tn.add_production(m.mk_false());

For benchmarks whose universally-quantified array variable has a deeply
nested array sort that unfolds to a Bool target sort (e.g. the forall over
r : (Array (Array Bool Bool) (Array Bool Bool)) in iss-6174/small.smt2),
these extra Bool leaves combine combinatorially with the select/store/eq
operators in term_enumeration. enum_terms then blows up and MBQI hangs:
the third check-sat, which previously returned quickly, now times out at
-T:20 (and even -T:60). The pre-existing max_count=20 bound limits how many
terms are inserted but not the enumerator's internal work.

Remove the two auxiliary Boolean productions. The commit's titular change
(setting m_is_auf = false in all cases) is benign for this benchmark and is
preserved; only the enumeration-blowup lines are dropped. After the fix the
benchmark returns "sat sat sat" with no timeout, and the third query's model
passes model_validate=true.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/smt/smt_model_finder.cpp

@@ -1413,8 +1413,6 @@ namespace smt {
                 // add other possible relevant functions such as equality over srt, Boolean operators
 
                 ast_mark visited;
-                tn.add_production(m.mk_true());
-                tn.add_production(m.mk_false());
                 for (enode *n : ctx->enodes()) {
                     if (!ctx->is_relevant(n))
                         continue;