Mark symbols introduced by named attributes as defined. (#3190)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 346675b6bd400dacc39a9dc60f18c07b05e21509..436e15d3231ad3b661b5649d3e3118a73ae95007 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1933,7 +1933,7 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
   // check that sexpr is a fresh function symbol, and reserve it
   reserveSymbolAtAssertionLevel(name);
   // define it
-  Expr func = mkVar(name, expr.getType());
+  Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED);
   // remember the last term to have been given a :named attribute
   setLastNamedTerm(expr, name);
   return func;