diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-23 16:01:13 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 15:17:37 -0400 |
commit | b3a4670710d3ffdc99879a1d27f37cf775af18eb (patch) | |
tree | afb6554dcf95cdd324384478a51e01c5d63c106b /src/parser/tptp | |
parent | c2972fc63ca6d49ffeaf0e8a9a39cad733790cd7 (diff) |
Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer
Diffstat (limited to 'src/parser/tptp')
-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 |