projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e4fd524) | patch
Fix length assumption for deq norm emp rule (#5623)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 11 Dec 2020 21:04:35 +0000 (15:04 -0600)
committerGitHub <noreply@github.com>
Fri, 11 Dec 2020 21:04:35 +0000 (15:04 -0600)
commit49215e6948aba1d6b762e28a7293581e25c2df8c
treec769369b913bb383c714ae68c575add32e3d06e1tree
parente4fd524b02054a3ac9724f184e55a983cb6cb6b9commit | diff
Fix length assumption for deq norm emp rule (#5623)

There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.

Fixes #5611.

Note this inference was not previously covered in our coverage build.
src/theory/strings/core_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 [new file with mode: 0644] blob