From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 17 Aug 2019 15:53:51 +0000 (-0500)
Subject: Mark symbols introduced by named attributes as defined. (#3190)
X-Git-Tag: cvc5-1.0.0~4008
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=340c647857663df289fe9d243175a20124615ab5;p=cvc5.git

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

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 346675b6b..436e15d32 100644
--- 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;