TermTranslator unhelpful rewrite.

[kunalsheth]

When fed the CVC5 term:
(let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (<= 0 _let_2) (<= 0 _let_1) (<= (+ _let_2 _let_1) 1) (not (p 0)) (p _let_1))))

The TermTranslator (to any solver), rewrites it as:
(let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (= (ite (<= 0 _let_2) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= 0 _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= (+ _let_2 _let_1) 1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (not (p 0)) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (p _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)))))

We would like the option to disable such a rewrite.

It appears this may be caused by two related bugs:

1. Because the AND has more than two children, execution goes into the if-statement linked below. We think we would like an option to manually disable this check and/or make smt-switch allow for ANDs to support more than two children. The translated term should have as similar a structure to the original term as possible.
   https://github.com/stanford-centaur/smt-switch/blob/f2d7d3d6dfccc0b4d6b604563acd34629bac884d/src/term_translator.cpp#L269C12-L269C12
2. It looks like cast_op and/or cast_term are being called twice upon themselves, leading to a Boolean-to-BV rewrite immediately followed by a BV-to-Boolean rewrite— which I do not think is the intended behavior, and we would also like to turn off.

[barrettcw]

This does look weird. Can you propose a fix and submit a PR?

[barrettcw]

@makaimann - low priority but could you have a look at this and see if you can tell us where the problem is?