projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c0d4ac3) | patch
Guard for non-unique skolems in term formula removal (#6179)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 22 Mar 2021 14:51:05 +0000 (09:51 -0500)
committerGitHub <noreply@github.com>
Mon, 22 Mar 2021 14:51:05 +0000 (09:51 -0500)
commit93fd4aed186c3dfa1b0fa7bec102f5b94edca322
tree331b0bd9dcc69c2355887db5ca5fd1a20d6a63e3tree
parentc0d4ac3d307b13c24471da5af2f916569a7f52b9commit | diff
Guard for non-unique skolems in term formula removal (#6179)

In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.

Fixes #6132.
src/expr/skolem_manager.h diff | blob | history
src/smt/term_formula_removal.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue6132-non-unique-skolem.smt2 [new file with mode: 0644] blob