SMT-LIB2の(線形)算術では除算は全域的で、ゼロ除算結果は単にunspecifiedというだけなのだけど、 当然除算の関数性から α=β のときには α/0=β/0 でなくてはならず、 これを実現するには結局EUFソルバとの理論結合が必要になるような。 というわけで、QF_LRAを実装するには結局QF_UFLRA相当の実装が必要になる気がする。