diff options
Diffstat (limited to 'src/parser/tptp/tptp.h')
| -rw-r--r-- | src/parser/tptp/tptp.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 96c608f77..eb49d7dcc 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -177,7 +177,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name, expr = getVariable(name); } else { Type t = term ? d_unsorted : getExprManager()->booleanType(); - expr = mkVar(name, t, true); // levelZero + expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero preemptCommand(new DeclareFunctionCommand(name, expr, t)); } } else { // Its an application @@ -187,7 +187,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name, std::vector<Type> sorts(args.size(), d_unsorted); Type t = term ? d_unsorted : getExprManager()->booleanType(); t = getExprManager()->mkFunctionType(sorts, t); - expr = mkVar(name, t, true); // levelZero + expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero preemptCommand(new DeclareFunctionCommand(name, expr, t)); } // args might be rationals, in which case we need to create |