1 2 3 4 5 6 7
(benchmark reject_nonlinear :logic QF_LRA :extrafuns ((n Real)) :status unknown :formula (= (/ n n) 1) )