if-then-else in SMT-LIB

[Cesare Tinelli]

Dear Shuvendu,

thanks for your additional insights on why it'd be good to have an
ITE construct of the form "if \phi then t1 else t2" in the SMT-LIB
language.
I guess the question is settled then :)

Cheers,


Cesare


Shuvendu Lahiri wrote:
> Dear all,
> 	We would like to add a few words about Jim's comment about
> if-then-else (ITE).
> 
> 	We feel that it is helpful to have if \phi then t1 else t2 in
> the language, at least for efficiency purpose. Here are a couple of reaons
> that we have encountered in our work with UCLID.
> 
[...]