Very similar test to the one in the issue #19 ``` (set-logic QF_ALIA) (declare-fun n () Int) (declare-fun f () Int) (assert (<= f (+ n 1))) (assert (<= n f)) (assert (distinct n f)) (assert (not (= f (+ n 1)))) (check-sat) ``` [interval_incompleteness_2.smt2](/uploads/56aead0bb4cbed7b59826947457bc9da/interval_incompleteness_2.smt2)