Rewrite (ite (not T) true T) = true not supported?

[maurobringolf]

Commit: b4e98013a8e2572545ec3f637dd1caa06e3f7207

Another case of an ite rewrite which seems reasonable to expect? Essentially the opposite case of cvc5/cvc5#6717.

$ cvc5 -q --strings-exp unknown.smt2
unknown
$ cvc4-1.8 -q --strings-exp unknown.smt2
unknown
$ cat unknown.smt2
(assert (ite (not (exists ((x Int)) (= "-" (str.substr "-" x (- 1 x))))) true (exists ((x Int)) (= "-" (str.substr "-" x (- 1 x))))))
(check-sat)

Note that the instance of T here is solvable on its own:

$ cvc5 -q --strings-exp known.smt2
sat
$ cvc4-1.8 -q --strings-exp known.smt2
sat
$ cat known.smt2
(assert (exists ((x Int)) (= "-" (str.substr "-" x (- 1 x)))))
(check-sat)

[ajreynol]

Notice that since quantifiers are parsed independently, the original problem is actually of the form (ite (not T) true S) where T and S are alpha-equivalent but syntactically distinct quantified formulas. Hence a simple rewrite does not apply here.

I'm marking this "performance", it would nevertheless be nice to solve this.