1 2 3 4 5 6 7 8 9 10 11 12
; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-sort U 0) (declare-fun x () U) (declare-fun y () U) (declare-fun a () U) (declare-fun b () U) (assert (not (sep (not (pto x a)) (pto y b)))) (check-sat)