[SMT-LIB] QF_AUFBV. difficulty, status, syntax.

[Trevor Alexander HANSEN]

Hi,

I'm new to the competition and have been looking through the QF_AUFBV 
benchmarks and have three questions.

In the newly addeded benchmarks, many have a status of "uknown". Some of the 
benchmarks with the unknown status are easy to solve. I understand that 
"uknown" status benchmarks are not included in the competition. Will the status 
of these benchmarks be updated before the competition?

I note that the difficulty of the new benchmarks isn't set. Also that the 
difficulty of existing benchmarks not updated. This year's contest rules state 
that the difficulty will be updated before selection begins. Is calculating the 
difficulty of the benchmarks something that happens after the benchmarks are 
frozen? Are the revised difficulties made available before the contest?

testcase7.stp.smt uses an "if_then_else" function. Now it's easy to see what it 
should do, and easy to parse it properly. It's implemented by most solvers. But 
is this function actually in the language?

Thanks,

Trevor