# What is the difference in heap configurations? Separation logic with CVC5 SMT solver

I am figuring out separation logic and trying to run simple examples in CVC5 smt solver. I am missing some core understanding of how pointers and values are treated there and I don't know where to look for more information.

I am sorry for the long snippets, but they are very simple.

## First query

(set-logic QF_ALL)
(set-info :smt-lib-version 2.6)

(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :produce-unsat-cores true)

; heap with uninterpreted sort as Data
(declare-sort Data 0)
; "single" element for the pointers to point to
(declare-const unit Data)
; Heap declaration
(declare-heap (Int Data))

; Two pointers
(declare-const left Int)
(declare-const right Int)

; constraints for better readability of the model
(assert (= (as sep.nil Int) 0))
(assert (>= left 0))
(assert (>= right 0))

; query itself
(assert (not
(sep
(pto left unit)
(pto right unit)
)
))

(check-sat)
(get-model)


### CVC5 output

sat
(
; cardinality of Data is 1
; rep: (as @Data_0 Data)
(define-fun unit () Data (as @Data_0 Data))
(define-fun left () Int 1)
(define-fun right () Int 2)
)
(heap
(sep (pto 2 (as @Data_0 Data)) (pto 1 (as @Data_0 Data)))
(= (as sep.nil Int) 0)
)


## Second query

(set-logic QF_ALL)
(set-info :smt-lib-version 2.6)

(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :produce-unsat-cores true)

; heap with uninterpreted sort as Data
(declare-sort Data 0)
; "single" element for the pointers to point to
(declare-const unit Data)
; Heap declaration
(declare-heap (Int Data))

; Two pointers
(declare-const left Int)
(declare-const right Int)

; constraints for better readability of the model
(assert (= (as sep.nil Int) 0))
(assert (>= left 0))
(assert (>= right 0))

; query itself
(assert
(sep
(pto left unit)
(pto right unit)
)
)

(check-sat)
(get-model)


### CVC5 output

sat
(
; cardinality of Data is 1
; rep: (as @Data_0 Data)
(define-fun unit () Data (as @Data_0 Data))
(define-fun left () Int 1)
(define-fun right () Int 2)
)
(heap
(sep (pto 2 unit) (pto 1 unit))
(= (as sep.nil Int) 0)
)


# Question about the second heap

(heap
(sep (pto 2 unit) (pto 1 unit))
(= (as sep.nil Int) 0)
)


Why the second heap satisfies (sep (pto left unit) (pto right unit)), despite both pointers pointing to the same unit?

# Question about the first heap

(heap
(sep (pto 2 (as @Data_0 Data)) (pto 1 (as @Data_0 Data)))
(= (as sep.nil Int) 0)
)


Why is this heap satisfies not (sep (pto left unit) (pto right unit) even with unit being equal to @Data_0, which works for the other query?

Why these similar-looking heaps are satisfying mutually exclusive conditions?

I am looking to some paper or documentation page for the in-depth explanation.

• Maybe try proofassistants.stackexchange.com
– Kai
Commented Feb 27, 2023 at 0:12
• @Kai, thank you, I will try if there are no answers here Commented Feb 27, 2023 at 10:17
• @Kai I'm not sure proofassistants is the right place to ask, as long as CVC5 and other SAT/SMT solvers are not proof assistants (they are automatic theorem provers)... Commented Feb 27, 2023 at 10:43