From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Thu, 30 Sep 2021 02:59:18 +0000 (-0500)
Subject: Print `str.is_digit` and `int.pow2` correctly. (#7276)
X-Git-Tag: cvc5-1.0.0~1154
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f998504d88e507bae22cdd7cc0dfd20f786ed99;p=cvc5.git

Print `str.is_digit` and `int.pow2` correctly. (#7276)
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fd98bdeca..0c107573f 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -965,7 +965,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::MULT:
   case kind::NONLINEAR_MULT: return "*";
   case kind::IAND: return "iand";
-  case kind::POW2: return "POW2";
+  case kind::POW2: return "int.pow2";
   case kind::EXPONENTIAL: return "exp";
   case kind::SINE: return "sin";
   case kind::COSINE: return "cos";
@@ -1169,6 +1169,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::STRING_LT: return "str.<";
   case kind::STRING_FROM_CODE: return "str.from_code";
   case kind::STRING_TO_CODE: return "str.to_code";
+  case Kind::STRING_IS_DIGIT: return "str.is_digit";
   case kind::STRING_ITOS: return "str.from_int";
   case kind::STRING_STOI: return "str.to_int";
   case kind::STRING_IN_REGEXP: return "str.in_re";