diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-08-31 14:26:26 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-08-31 14:26:26 +0200 |
| commit | 949dc989f72c680b98a4f7c4e52616b393237b52 (patch) | |
| tree | 6e73970da5745515292a9192e7e5f74ca87dac66 /src/theory/theory_model.cpp | |
| parent | 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4 (diff) | |
Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from user input, add regressions. (#1060)
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 75bc40af7..840bbd027 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -137,8 +137,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c return (*it).second; } Node ret = n; - if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || - ( n.getKind() == kind::CARDINALITY_CONSTRAINT && options::ufssMode()!=theory::uf::UF_SS_FULL ) ) { + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ) { // We should have terms, thanks to TheoryQuantifiers::collectModelInfo(). // However, if the Decision Engine stops us early, there might be a // quantifier that isn't assigned. In conjunction with miniscoping, this |