test/regress/regress0/sep/simple-080420-const-sets.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_ALL)
(set-option :produce-models true)
(set-info :status sat)
(declare-heap (Int Int))
(declare-fun x () Int)

; works
;(assert (sep (pto 1 2) (pto 5 6) (pto x 8)))

; didn't work due to sets rewriter
(assert (sep (pto 1 2) (pto 5 6) (pto 7 8)))

(check-sat)