summaryrefslogtreecommitdiff
path: root/src/parser/tptp/Tptp.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/tptp/Tptp.g')
-rw-r--r--src/parser/tptp/Tptp.g4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 63774a087..068e92cd7 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -327,7 +327,7 @@ variable[CVC4::Expr & expr]
if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)){
expr = PARSER_STATE->getVariable(name);
} else {
- expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted);
+ expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
if(PARSER_STATE->cnf) PARSER_STATE->addFreeVar(expr);
}
}
@@ -402,7 +402,7 @@ bindvariable[CVC4::Expr & expr]
: UPPER_WORD
{
std::string name = AntlrInput::tokenText($UPPER_WORD);
- expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted);
+ expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
}
;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback