Fix collect model values for sequences of sequences (#5579)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 8 Dec 2020 04:46:22 +0000 (22:46 -0600)
committerGitHub <noreply@github.com>
Tue, 8 Dec 2020 04:46:22 +0000 (22:46 -0600)
commit3223d3c765b87db9d87a7ca65c4b7cf5dc9a7885
tree2246f2e133cd8f9a8e6a4da62f13c8b9d4df81d7
parent57241d382490eed0c480f234dc8cf1c18c1fa525
Fix collect model values for sequences of sequences (#5579)

Fixes #5543.

Recently we changed our model construction for sequences here: #5391.

This fix is not safe for sequences of sequences, where Valuation::getModelValue should not be called, since the argument of the seq.unit is not a shared term.

This makes our model construction for sequences more robust, however I'm not sure this is the end solution. In particular, it is still questionable whether we should call Valuation::getModelValue at all (consider sequences of theories whose model construction comes after strings), or for cases of (seq.unit x) where x is a sequence or string that does not have a concrete value. Regardless, this PR could be merged in the meantime since it should definitely fix some of the current issues.
src/theory/strings/theory_strings.cpp
test/regress/CMakeLists.txt
test/regress/regress0/seq/issue5543-unit-cmv.smt2 [new file with mode: 0644]