projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eaf29fe) | patch
Infer emptiness instead of splitting when a string equality rewrites to a constant...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 23 Aug 2019 22:27:05 +0000 (17:27 -0500)
committerGitHub <noreply@github.com>
Fri, 23 Aug 2019 22:27:05 +0000 (17:27 -0500)
commit0faead1572109c1d7cb3d67647da02d0b4600a20
treee0bd28feb049be6a36a63fd73df37f9d3cc7aa54tree
parenteaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5commit | diff
 Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218)
src/theory/strings/infer_info.cpp diff | blob | history
src/theory/strings/infer_info.h diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue3217.smt2 [new file with mode: 0644] blob