[LRA] can only solve after manually simplifying `(or true c)` to `true` or `c`, knowing that the goal is satisfiable with `c`

On the branch hra/lra_relop_norm_opt, commit d3b4c71a, that makes the normalization of relational operations to le optional, colibri2 can't solve the test relop_norm_reg.smt2 with the option --lra-relop-norm:

unknown-branch-cut                       
(steps 242456)

But it can solve it if we replace (or true (< (- _B_ra_rb_gb t_A_ra_) 0)) with true:

sat                                       
(steps 295)

Or if we replace (or true (< (- _B_ra_rb_gb t_A_ra_) 0)) with (< (- _B_ra_rb_gb t_A_ra_) 0) (knowing that the goal stays satisfiable):

sat                                      
(steps 379)