[578] % z3 small.smt2
Segmentation fault
[579] % 
[579] % cat small.smt2
(set-option :rewriter.arith_lhs true)
(set-option :rewriter.sort_sums true)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (> (+ (* 2 a) (* (- 2) b)) 0))
(check-sat-using ufbv)
[580] %