From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Jul 2021 01:52:15 +0000 (-0500)
Subject: Miscellaneous fixes from proof-new (#6914)
X-Git-Tag: cvc5-1.0.0~1448
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=22ef16d1108dd0e42da203ca4d453fbdd128a8d6;p=cvc5.git

Miscellaneous fixes from proof-new (#6914)
---

diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index b619a36e2..507cebab3 100644
--- a/src/expr/bound_var_manager.h
+++ b/src/expr/bound_var_manager.h
@@ -77,7 +77,7 @@ class BoundVarManager
   Node mkBoundVar(Node n, const std::string& name, TypeNode tn)
   {
     Node v = mkBoundVar<T>(n, tn);
-    setNameAttr(n, name);
+    setNameAttr(v, name);
     return v;
   }
   //---------------------------------- utilities for computing Node hash
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b5a8472e6..bf26b80ee 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -824,8 +824,8 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::PRODUCT:
   case kind::TRANSPOSE:
   case kind::TCLOSURE:
-    out << smtKindString(k, d_variant) << " ";
-    break;
+  case kind::IDEN:
+  case kind::JOIN_IMAGE: out << smtKindString(k, d_variant) << " "; break;
   case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break;
   case kind::SINGLETON:
   {
@@ -1237,6 +1237,11 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
   case kind::INT_TO_BITVECTOR: return "int2bv";
 
+  // datatypes theory
+  case kind::APPLY_TESTER: return "is";
+  case kind::APPLY_UPDATER: return "update";
+
+  // set theory
   case kind::UNION: return "union";
   case kind::INTERSECTION: return "intersection";
   case kind::SETMINUS: return "setminus";
@@ -1254,6 +1259,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::PRODUCT: return "product";
   case kind::TRANSPOSE: return "transpose";
   case kind::TCLOSURE: return "tclosure";
+  case kind::IDEN: return "iden";
+  case kind::JOIN_IMAGE: return "join_image";
 
   // bag theory
   case kind::BAG_TYPE: return "Bag";