Incompleteness on integer reasoning with intervals
Colibri2 returns unknown-branch-cut on:
(set-logic ALL)
(declare-fun n () Int)
(declare-fun m () Int)
(assert (distinct n m))
(assert (<= n m (+ n 1)))
(assert (distinct m (+ n 1)))
(check-sat)Colibri2 returns unknown-branch-cut on:
(set-logic ALL)
(declare-fun n () Int)
(declare-fun m () Int)
(assert (distinct n m))
(assert (<= n m (+ n 1)))
(assert (distinct m (+ n 1)))
(check-sat)