From 4ac14c09322f234ba2a201e0d281664338fd9ee0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 28 Feb 2020 22:30:40 -0600 Subject: Fix assertion related to assignability in the model. (#3843) Fixes #3813. It appears that an assertion was hardcoded to check whether a term was a variable or APPLY_UF application whereas this check should use isAssignable. This avoids an assertion failure on the given benchmark. --- src/theory/theory_model_builder.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/theory/theory_model_builder.cpp') 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()) { -- cgit v1.2.3