Miscellaneous fixes from proof-new (#6914)

diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index b619a36e2b584e71630114c66f8dfeb8ce271551..507cebab3d97f4e642779a690398f168b943b734 100644 (file)
--- 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 b5a8472e6ddf16410ca80db820da29abebc6a0a4..bf26b80ee938a537e725cf8da1e24bfc114f6584 100644 (file)
--- 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";