diff --git a/src/state.cpp b/src/state.cpp index 514c7ed..a90d1e4 100644 --- a/src/state.cpp +++ b/src/state.cpp @@ -179,16 +179,16 @@ Expr State::mkExpr(Kind k, const std::vector& children) Expr hd = children[0]; size_t i = 1; Expr curr = children[isLeft ? i : nchild-i]; - AppInfo * ail = getAppInfo(curr.get()); std::vector cc{hd, nullptr, nullptr}; size_t nextIndex = isLeft ? 2 : 1; size_t prevIndex = isLeft ? 1 : 2; - if (ail!=nullptr) + if (ai->d_attrConsTerm!=nullptr) { - // if the last term is not marked as a list variable and - // we have a null terminator, then we insert the null terminator - if (!ail->hasAttribute(Attr::LIST) && ai->d_attrConsTerm!=nullptr) + AppInfo * ail = getAppInfo(curr.get()); + if (ail!=nullptr && !ail->hasAttribute(Attr::LIST)) { + // if the last term is not marked as a list variable and + // we have a null terminator, then we insert the null terminator cc[prevIndex] = ai->d_attrConsTerm; cc[nextIndex] = curr; curr = mkExprInternal(Kind::APPLY, cc); @@ -221,7 +221,7 @@ Expr State::mkExpr(Kind k, const std::vector& children) } // note this could loop return mkExpr(Kind::APPLY, cchildren); - } + } break; default: break; diff --git a/tests/or-list-null-term.smt2 b/tests/or-list-null-term.smt2 index 798b3da..1c8b1a5 100644 --- a/tests/or-list-null-term.smt2 +++ b/tests/or-list-null-term.smt2 @@ -1,5 +1,3 @@ - - (declare-const true Bool) (declare-const false Bool)