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 414c2f6b0..4e73fa6cf 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -527,7 +527,7 @@ fofLogicFormula[CVC4::Expr& expr]
( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
{ switch(na) {
case tptp::NA_IFF:
- expr = MK_EXPR(kind::IFF,expr,expr2);
+ expr = MK_EXPR(kind::EQUAL,expr,expr2);
break;
case tptp::NA_REVIFF:
expr = MK_EXPR(kind::XOR,expr,expr2);
@@ -662,7 +662,7 @@ tffLogicFormula[CVC4::Expr& expr]
( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
{ switch(na) {
case tptp::NA_IFF:
- expr = MK_EXPR(kind::IFF,expr,expr2);
+ expr = MK_EXPR(kind::EQUAL,expr,expr2);
break;
case tptp::NA_REVIFF:
expr = MK_EXPR(kind::XOR,expr,expr2);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback