projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e0009c8) | patch
Fix preregistration in TheorySep before declare-heap (#5411)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Nov 2020 02:27:38 +0000 (20:27 -0600)
committerGitHub <noreply@github.com>
Wed, 11 Nov 2020 02:27:38 +0000 (20:27 -0600)
commit59d8647b04f86421949390a3e958ffdf0df07665
treea916fa77cb38bb24da805b8e444c3584931652c8tree
parente0009c822488a2c39f8907e37333409c1191d47bcommit | diff
Fix preregistration in TheorySep before declare-heap (#5411)

Followup to fix for #5343. This catches cases where separation logic constraints are preregistered to TheorySep before the heap has been declared, which should also result in an error.
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/sep/theory_sep.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sep/issue5343-err.smt2 [new file with mode: 0644] blob