Skip `str.code` inferences for sequence eqcs (#7644)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 13 Nov 2021 20:24:44 +0000 (12:24 -0800)
committerGitHub <noreply@github.com>
Sat, 13 Nov 2021 20:24:44 +0000 (20:24 +0000)
commitf5b8f74ec2f7297cd54e19459f039416df67f862
tree1efe1609302ef1d669c0bb377585088de869a6fa
parent805205a2047eeae7842b1c534859b52fa204ee0e
Skip `str.code` inferences for sequence eqcs (#7644)

Fixes cvc5/cvc5-projects#340. Type checking
failed because cvc5 was trying to construct a term (str.to_code (seq.unit false)). We do not allow the construction of terms
(str.to_code t) where t is not of type string. This commit fixes the
issue by skipping sequence equivalence classes when doing inferences
related to str.to_code.

Note that the regression test is slightly different from the original
unit test. It asserts that the index passed to seq.nth is
non-negative, which ensures that we can check the resulting model. I
have checked that the modified regression test triggers the issue before
the change in this commit.
src/theory/strings/base_solver.cpp
src/theory/strings/base_solver.h
src/theory/strings/core_solver.cpp
src/theory/strings/theory_strings.cpp
test/regress/CMakeLists.txt
test/regress/regress0/seq/proj-issue340.smt2 [new file with mode: 0644]