unsat
((= (fp.abs a) b))