From 94c687bb12f3ba89225886b3b3eeea3f0dfdfd0a Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 7 Jan 2021 17:06:33 -0300
Subject: [PATCH] Fix warning in TPTP parser  (#5752)

---
 src/parser/tptp/Tptp.g | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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        : '<=>';
-- 
2.30.2