Make `STRINGS_CTN_DECOMPOSE` an explicit conflict (#6663)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 2 Jun 2021 13:50:51 +0000 (06:50 -0700)
committerGitHub <noreply@github.com>
Wed, 2 Jun 2021 13:50:51 +0000 (13:50 +0000)
commitc54fe84863ce4257bd466a95ec42d7a6100d3c19
tree33ad856f7687f5faa234093350407e62a7e0e973
parent66cdf5254bc58ecff335321478e73c8c0d6df296
Make `STRINGS_CTN_DECOMPOSE` an explicit conflict  (#6663)

Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.
src/theory/strings/extf_solver.cpp
test/regress/CMakeLists.txt
test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 [new file with mode: 0644]