From 340c647857663df289fe9d243175a20124615ab5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 17 Aug 2019 10:53:51 -0500 Subject: [PATCH] Mark symbols introduced by named attributes as defined. (#3190) --- src/parser/smt2/smt2.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; -- 2.30.2