From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 2 Jun 2018 19:18:24 +0000 (-0500)
Subject:  Fix assertion involving unassigned Boolean eqc in model (#2050)
X-Git-Tag: cvc5-1.0.0~4982
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6de92e6a6ac4dd81ff7f65bf33bddfabfc3e2c48;p=cvc5.git

 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 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())
           {