;some simple tests for quantifier elimination over the rationals (set-option :print-terms-cse false) (set-logic LRA) (simplify (=> (exists ((x Real)) (=> (or (= x (+ 1 2)) (= (* x 3) 6)) (>= (* 4 x) 4))) (forall ((x Real)) (=> (and (= x 5) (not (= x 6))) (<= x 7))))) (simplify (exists ((x Real)) (=> (= x (+ 1 2)) (>= (* 4 x) 4)))) (simplify (exists ((x Real)) (and (< (+ (* 3 x) 1) 10) (> (- (* 7 x) 6) 7)))) (declare-fun y () Real) (declare-fun z () Real) (simplify (exists ((x Real)) (and (> (* 2 x) y) (< (* 3 x) z)))) (simplify (forall ((x Real)) (forall ((y Real)) (=> (> x y) (>= x y))))) (simplify (forall ((x Real)) (not (> x x))))