From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 7 Jan 2021 20:06:33 +0000 (-0300)
Subject: Fix warning in TPTP parser  (#5752)
X-Git-Tag: cvc5-1.0.0~2396
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94c687bb12f3ba89225886b3b3eeea3f0dfdfd0a;p=cvc5.git

Fix warning in TPTP parser  (#5752)
---

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 6b66b5422..0c16e472d 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -921,7 +921,7 @@ thfQuantifier[CVC4::api::Kind& kind]
   | LAMBDA_TOK { kind = api::LAMBDA; }
   | CHOICE_TOK
     {
-        UNSUPPORTED("Choice operator");
+      UNSUPPORTED("Choice operator");
     }
   | DEF_DESC_TOK
     {
@@ -1621,7 +1621,7 @@ NOT_TOK        : '~';
 FORALL_TOK     : '!';
 EXISTS_TOK     : '?';
 LAMBDA_TOK     : '^';
-WITNESS_TOK     : '@+';
+CHOICE_TOK     : '@+';
 DEF_DESC_TOK   : '@-';
 AND_TOK        : '&';
 IFF_TOK        : '<=>';