switch default SMT logic to QF_AUFLIA

We really should have been using a UF logic already, given we generate
declare-fun commands. However, seems most solvers are happy to accept these in
non-UF logics as well.