projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 17d5e26) | patch
Fix pto handling for heaps that are not a subset of the base heap (#8942)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 7 Jul 2022 16:26:00 +0000 (11:26 -0500)
committerGitHub <noreply@github.com>
Thu, 7 Jul 2022 16:26:00 +0000 (16:26 +0000)
commitf08aa56f710b46da5c2b5157c102062e9a39e0b9
treebf9856bfcee9734d60aada5d6260b6d6b90acf9ctree
parent17d5e26a9a0aac458cd8c9a0bf8d99b62efadc52commit | diff
Fix pto handling for heaps that are not a subset of the base heap (#8942)

These require a downwards rule to be compatible with our propagation rules for pto.

Fixes #8863.
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/sep/theory_sep.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/sep/issue8863-downwards-pto.smt2 [new file with mode: 0644] blob