diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-07 22:46:22 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-07 22:46:22 -0600 |
| commit | 3223d3c765b87db9d87a7ca65c4b7cf5dc9a7885 (patch) | |
| tree | 2246f2e133cd8f9a8e6a4da62f13c8b9d4df81d7 /src/theory/strings/term_registry.cpp | |
| parent | 57241d382490eed0c480f234dc8cf1c18c1fa525 (diff) | |
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.
Diffstat (limited to 'src/theory/strings/term_registry.cpp')
0 files changed, 0 insertions, 0 deletions