projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f41d71c) | patch
Ensure sequences of Booleans generate Boolean term variable skolems when applicable...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 May 2021 13:30:42 +0000 (08:30 -0500)
committerGitHub <noreply@github.com>
Wed, 12 May 2021 13:30:42 +0000 (13:30 +0000)
commit111f98a41b488b8124fbecd28dba17465ea30786
treeaaec0192960bdb3e47efc39917c4e2db23ea1f5dtree
parentf41d71cbf1946a5ee5a63c062a23c7426ec5e87dcommit | diff
Ensure sequences of Booleans generate Boolean term variable skolems when applicable (#6529)

Fixes #6510.

This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/strings/skolem_cache.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue6510-seq-bool.smt2 [new file with mode: 0644] blob