(set-logic QF_LIA) (declare-fun x () Int) (assert (not (=> (= (- x 3) 7) (>= x 10)))) (check-sat) (exit)