diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_model_builder.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index e15211847..a96f29ada 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -788,13 +788,12 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) { Assert(!evaluable || assignOne); // 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. + // Boolean type, then the term must be assignable. // 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); + Assert(!t.isBoolean() || isAssignable(*i2)); Node n; if (itAssigner != eqcToAssigner.end()) { |