diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-17 10:53:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-17 10:53:51 -0500 |
| commit | 340c647857663df289fe9d243175a20124615ab5 (patch) | |
| tree | 6ecac095c3a551c2a45332234e933e311530aa01 | |
| parent | 38e1a8bd1d8ad2e4fab4c89c46bfab88223762eb (diff) | |
Mark symbols introduced by named attributes as defined. (#3190)
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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; |