diff options
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index f91a413e3..5024d17ac 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -666,7 +666,14 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) if (assignable) { Assert(!evaluable || assignOne); - Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); + // this assertion ensures that if we are assigning to a term of + // Boolean type, then the term is either a variable or an APPLY_UF. + // Note we only assign to terms of Boolean type if the term occurs in + // a singleton equivalence class; otherwise the term would have been + // in the equivalence class of true or false and would not need + // assigning. + Assert(!t.isBoolean() || (*i2).isVar() + || (*i2).getKind() == kind::APPLY_UF); Node n; if (t.getCardinality().isInfinite()) { |