projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cf5cd99) | patch
Fix subtyping for sets care graph (#6278)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 5 Apr 2021 15:21:55 +0000 (10:21 -0500)
committerGitHub <noreply@github.com>
Mon, 5 Apr 2021 15:21:55 +0000 (15:21 +0000)
commit73bc16fbba65ca8d8cdc9dd6674ae9280658ee9a
tree41175283436792bb3332bc465793d901ff55544etree
parentcf5cd9981f92985e647df5bb9244679715951e8ccommit | diff
Fix subtyping for sets care graph (#6278)

We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals.

Fixes #5705.
src/theory/sets/theory_sets_private.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sets/issue5705-cg-subtyping.smt2 [new file with mode: 0644] blob