Fix assertion involving unassigned Boolean eqc in model (#2050)

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index f91a413e3e8a744ddd88da912973b09ea424f895..5024d17ace1b360c891fd0689e6c3c1ec58ad0af 100644 (file)
--- 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())
           {