Do not mark extended functions as reduced based on decomposing contains (#5407)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 10 Nov 2020 21:48:05 +0000 (15:48 -0600)
committerGitHub <noreply@github.com>
Tue, 10 Nov 2020 21:48:05 +0000 (15:48 -0600)
commite0009c822488a2c39f8907e37333409c1191d47b
treebfc4c40a5d8789769ab5d4827aa9562986e0f475
parentcef8ceaf4cd81863171363fe54a97921361d1de9
Do not mark extended functions as reduced based on decomposing contains (#5407)

Fixes #5381.
src/smt/check_models.cpp
src/theory/strings/extf_solver.cpp
test/regress/CMakeLists.txt
test/regress/regress2/strings/issue5381.smt2 [new file with mode: 0644]