From 6de92e6a6ac4dd81ff7f65bf33bddfabfc3e2c48 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 2 Jun 2018 14:18:24 -0500 Subject: [PATCH] Fix assertion involving unassigned Boolean eqc in model (#2050) --- src/theory/theory_model_builder.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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()) { -- 2.30.2